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

Theorem biimp3a 1466
Description: Infer implication from a logical equivalence. Similar to biimpa 480. (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 480 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
323impa 1107 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  nn0addge1  11935  nn0addge2  11936  nn0sub2  12035  eluzp1p1  12262  uznn0sub  12269  uzinfi  12320  iocssre  12809  icossre  12810  iccssre  12811  lincmb01cmp  12877  iccf1o  12878  fzosplitprm1  13146  subfzo0  13158  modfzo0difsn  13310  hashprb  13758  pfxpfx  14065  eflt  15465  fldivndvdslt  15758  prmdiv  16115  hashgcdlem  16118  vfermltl  16131  coprimeprodsq  16138  pythagtrip  16164  difsqpwdvds  16216  cshwshashlem2  16425  odinf  18685  odcl2  18687  slesolex  21290  tgtop11  21590  restntr  21790  hauscmplem  22014  icchmeo  23549  pi1xfr  23663  sinq12gt0  25103  tanord1  25132  gausslemma2dlem1a  25952  axsegconlem6  26719  lfuhgr1v0e  27047  crctcshwlkn0lem6  27604  crctcshwlkn0lem7  27605  clwlkclwwlkf1lem2  27793  s2elclwwlknon2  27892  eucrctshift  28031  eucrct2eupth  28033  nv1  28461  lnolin  28540  br8d  30377  fzm1ne1  30541  ismntd  30695  mntf  30696  cycpmco2lem6  30826  ballotlemfc0  31858  ballotlemfcc  31859  ballotlemrv2  31887  fisshasheq  32460  br8  33100  br6  33101  br4  33102  bj-imdiridlem  34595  ismtyima  35234  ismtybndlem  35237  ghomlinOLD  35319  ghomidOLD  35320  cvrcmp2  36573  atcvrj2  36722  1cvratex  36762  lplnric  36841  lplnri1  36842  lnatexN  37068  ltrnateq  37470  ltrnatneq  37471  cdleme46f2g2  37782  cdleme46f2g1  37783  dibelval1st  38438  dibelval2nd  38441  dicelval1sta  38476  hlhilphllem  39248  jm2.17b  39889  bi123impia  41182  sineq0ALT  41630  eliccre  42129  ioomidp  42138  smfinflem  43435  iccpartiltu  43926  goldbachthlem1  44049  evengpop3  44303  rnghmresel  44575  rhmresel  44621  itcovalsuc  45068
  Copyright terms: Public domain W3C validator