Theorem biimp3a 1470

Description: Infer implication from a logical equivalence. Similar to biimpa 478. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
biimp3a.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
biimp3a	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem biimp3a

Step	Hyp	Ref	Expression
1		biimp3a.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	biimpa 478	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1111	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  onomeneq  9228  nn0addge1  12518  nn0addge2  12519  nn0sub2  12623  eluzp1p1  12850  uznn0sub  12861  uzinfi  12912  iocssre  13404  icossre  13405  iccssre  13406  lincmb01cmp  13472  iccf1o  13473  fzosplitprm1  13742  subfzo0  13754  modfzo0difsn  13908  hashprb  14357  pfxpfx  14658  eflt  16060  fldivndvdslt  16357  prmdiv  16718  hashgcdlem  16721  vfermltl  16734  coprimeprodsq  16741  pythagtrip  16767  difsqpwdvds  16820  cshwshashlem2  17030  odinf  19431  odcl2  19433  slesolex  22184  tgtop11  22485  restntr  22686  hauscmplem  22910  icchmeo  24457  pi1xfr  24571  sinq12gt0  26017  tanord1  26046  gausslemma2dlem1a  26868  sltn0  27400  axsegconlem6  28211  lfuhgr1v0e  28542  crctcshwlkn0lem6  29100  crctcshwlkn0lem7  29101  clwlkclwwlkf1lem2  29289  s2elclwwlknon2  29388  eucrctshift  29527  eucrct2eupth  29529  nv1  29959  lnolin  30038  br8d  31870  fzm1ne1  32031  ismntd  32185  mntf  32186  cycpmco2lem6  32321  ballotlemfc0  33522  ballotlemfcc  33523  ballotlemrv2  33551  fisshasheq  34135  br8  34757  br6  34758  br4  34759  gg-icchmeo  35201  bj-imdiridlem  36114  ismtyima  36719  ismtybndlem  36722  ghomlinOLD  36804  ghomidOLD  36805  cvrcmp2  38202  atcvrj2  38352  1cvratex  38392  lplnric  38471  lplnri1  38472  lnatexN  38698  ltrnateq  39100  ltrnatneq  39101  cdleme46f2g2  39412  cdleme46f2g1  39413  dibelval1st  40068  dibelval2nd  40071  dicelval1sta  40106  hlhilphllem  40882  jm2.17b  41748  bi123impia  43298  sineq0ALT  43746  eliccre  44266  ioomidp  44275  smfinflem  45581  iccpartiltu  46138  goldbachthlem1  46261  evengpop3  46514  rnghmresel  46910  rhmresel  46956  itcovalsuc  47401