Theorem biimp3a 1495

Description: Infer implication from a logical equivalence. Similar to biimpa 481. (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 481	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1125	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  vtoclegft  3557  onomeneq  9194  nn0addge1  12546  nn0addge2  12547  nn0sub2  12653  eluzp1p1  12886  uznn0sub  12893  uzinfi  12948  iocssre  13450  icossre  13451  iccssre  13452  lincmb01cmp  13518  iccf1o  13519  fzosplitprm1  13803  subfzo0  13817  modfzo0difsn  13975  hashprb  14429  pfxpfx  14741  eflt  16169  fldivndvdslt  16470  prmdiv  16840  hashgcdlem  16843  vfermltl  16857  coprimeprodsq  16864  pythagtrip  16890  difsqpwdvds  16943  cshwshashlem2  17152  odinf  19629  odcl2  19631  rnghmresel  20701  rhmresel  20730  slesolex  22804  tgtop11  23104  restntr  23304  hauscmplem  23528  icchmeo  25065  pi1xfr  25179  sinq12gt0  26634  tanord1  26664  gausslemma2dlem1a  27491  ltsn0  28061  onltn0s  28513  pw2cut  28615  axsegconlem6  29209  lfuhgr1v0e  29541  crctcshwlkn0lem6  30101  crctcshwlkn0lem7  30102  clwlkclwwlkf1lem2  30293  s2elclwwlknon2  30392  eucrctshift  30531  eucrct2eupth  30533  nv1  30964  lnolin  31043  br8d  32890  fzm1ne1  33070  ismntd  33241  mntf  33242  cycpmco2lem6  33388  ballotlemfc0  34824  ballotlemfcc  34825  ballotlemrv2  34853  fisshasheq  35501  br8  36143  br6  36144  br4  36145  cgsex2gd  37664  bj-imdiridlem  37712  ismtyima  38337  ismtybndlem  38340  ghomlinOLD  38422  ghomidOLD  38423  cvrcmp2  39943  atcvrj2  40092  1cvratex  40132  lplnric  40211  lplnri1  40212  lnatexN  40438  ltrnateq  40840  ltrnatneq  40841  cdleme46f2g2  41152  cdleme46f2g1  41153  dibelval1st  41808  dibelval2nd  41811  dicelval1sta  41846  hlhilphllem  42618  jm2.17b  43575  bi123impia  45086  sineq0ALT  45532  eliccre  46108  ioomidp  46117  smfinflem  47418  submodlt  47977  muldvdsfacgt  48007  iccpartiltu  48055  goldbachthlem1  48181  evengpop3  48447  gpgcubic  48728  gpg5nbgr3star  48730  itcovalsuc  49327