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 475. (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 475 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
323impa 1107 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  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 206  df-an 395  df-3an 1086
This theorem is referenced by:  onomeneq  9262  nn0addge1  12570  nn0addge2  12571  nn0sub2  12675  eluzp1p1  12902  uznn0sub  12913  uzinfi  12964  iocssre  13458  icossre  13459  iccssre  13460  lincmb01cmp  13526  iccf1o  13527  fzosplitprm1  13797  subfzo0  13809  modfzo0difsn  13963  hashprb  14414  pfxpfx  14716  eflt  16119  fldivndvdslt  16416  prmdiv  16787  hashgcdlem  16790  vfermltl  16803  coprimeprodsq  16810  pythagtrip  16836  difsqpwdvds  16889  cshwshashlem2  17099  odinf  19561  odcl2  19563  rnghmresel  20598  rhmresel  20627  slesolex  22675  tgtop11  22976  restntr  23177  hauscmplem  23401  icchmeo  24956  icchmeoOLD  24957  pi1xfr  25073  sinq12gt0  26535  tanord1  26564  gausslemma2dlem1a  27394  sltn0  27928  axsegconlem6  28856  lfuhgr1v0e  29190  crctcshwlkn0lem6  29749  crctcshwlkn0lem7  29750  clwlkclwwlkf1lem2  29938  s2elclwwlknon2  30037  eucrctshift  30176  eucrct2eupth  30178  nv1  30608  lnolin  30687  br8d  32530  fzm1ne1  32691  ismntd  32854  mntf  32855  cycpmco2lem6  33009  ballotlemfc0  34326  ballotlemfcc  34327  ballotlemrv2  34355  fisshasheq  34942  br8  35578  br6  35579  br4  35580  bj-imdiridlem  36892  ismtyima  37504  ismtybndlem  37507  ghomlinOLD  37589  ghomidOLD  37590  cvrcmp2  38982  atcvrj2  39132  1cvratex  39172  lplnric  39251  lplnri1  39252  lnatexN  39478  ltrnateq  39880  ltrnatneq  39881  cdleme46f2g2  40192  cdleme46f2g1  40193  dibelval1st  40848  dibelval2nd  40851  dicelval1sta  40886  hlhilphllem  41662  jm2.17b  42619  bi123impia  44165  sineq0ALT  44613  eliccre  45123  ioomidp  45132  smfinflem  46438  iccpartiltu  46994  goldbachthlem1  47117  evengpop3  47370  itcovalsuc  48055
  Copyright terms: Public domain W3C validator