Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimp3a Structured version   Visualization version   GIF version

Theorem biimp3a 1581
 Description: Infer implication from a logical equivalence. Similar to biimpa 502. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
biimp3a.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
biimp3a ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem biimp3a
StepHypRef Expression
1 biimp3a.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21biimpa 502 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
323impa 1101 1 ((𝜑𝜓𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074 This theorem is referenced by:  nn0addge1  11531  nn0addge2  11532  nn0sub2  11630  eluzp1p1  11905  uznn0sub  11912  uzinfi  11961  iocssre  12446  icossre  12447  iccssre  12448  lincmb01cmp  12508  iccf1o  12509  fzosplitprm1  12772  subfzo0  12784  modfzo0difsn  12936  hashprb  13377  swrd0fv  13639  eflt  15046  fldivndvdslt  15340  prmdiv  15692  hashgcdlem  15695  vfermltl  15708  coprimeprodsq  15715  pythagtrip  15741  difsqpwdvds  15793  cshwshashlem2  16005  odinf  18180  odcl2  18182  slesolex  20690  tgtop11  20988  restntr  21188  hauscmplem  21411  icchmeo  22941  pi1xfr  23055  sinq12gt0  24458  tanord1  24482  gausslemma2dlem1a  25289  axsegconlem6  26001  lfuhgr1v0e  26345  crctcshwlkn0lem6  26918  crctcshwlkn0lem7  26919  clwlkclwwlkf1lem2  27128  s2elclwwlknon2  27252  eucrctshift  27395  eucrct2eupth  27397  nv1  27839  lnolin  27918  br8d  29729  ballotlemfc0  30863  ballotlemfcc  30864  ballotlemrv2  30892  br8  31953  br6  31954  br4  31955  ismtyima  33915  ismtybndlem  33918  ghomlinOLD  34000  ghomidOLD  34001  cvrcmp2  35074  atcvrj2  35222  1cvratex  35262  lplnric  35341  lplnri1  35342  lnatexN  35568  ltrnateq  35971  ltrnatneq  35972  cdleme46f2g2  36283  cdleme46f2g1  36284  dibelval1st  36940  dibelval2nd  36943  dicelval1sta  36978  hlhilphllem  37753  jm2.17b  38030  bi123impia  39197  sineq0ALT  39672  eliccre  40231  ioomidp  40243  smfinflem  41529  iccpartiltu  41868  pfxpfx  41925  repswpfx  41946  goldbachthlem1  41967  evengpop3  42196  rnghmresel  42474  rhmresel  42520
 Copyright terms: Public domain W3C validator