Theorem biimp3a 1498

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 1127	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1105

This theorem is referenced by:  vtoclegft  3548  onomeneq  9194  nn0addge1  12545  nn0addge2  12546  nn0sub2  12652  eluzp1p1  12885  uznn0sub  12892  uzinfi  12947  iocssre  13449  icossre  13450  iccssre  13451  lincmb01cmp  13517  iccf1o  13518  fzosplitprm1  13803  subfzo0  13817  modfzo0difsn  13975  hashprb  14429  pfxpfx  14741  eflt  16168  fldivndvdslt  16469  prmdiv  16839  hashgcdlem  16842  vfermltl  16856  coprimeprodsq  16863  pythagtrip  16889  difsqpwdvds  16942  cshwshashlem2  17151  odinf  19628  odcl2  19630  rnghmresel  20719  rhmresel  20748  slesolex  22839  tgtop11  23139  restntr  23339  hauscmplem  23563  icchmeo  25100  pi1xfr  25214  sinq12gt0  26672  tanord1  26702  gausslemma2dlem1a  27529  ltsn0  28099  onltn0s  28551  pw2cut  28653  axsegconlem6  29272  lfuhgr1v0e  29604  crctcshwlkn0lem6  30164  crctcshwlkn0lem7  30165  clwlkclwwlkf1lem2  30356  s2elclwwlknon2  30455  eucrctshift  30594  eucrct2eupth  30596  nv1  31027  lnolin  31106  br8d  32953  fzm1ne1  33133  ismntd  33304  mntf  33305  cycpmco2lem6  33451  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemrv2  34912  fisshasheq  35606  br8  36248  br6  36249  br4  36250  cgsex2gd  37781  bj-imdiridlem  37829  ismtyima  38454  ismtybndlem  38457  ghomlinOLD  38539  ghomidOLD  38540  cvrcmp2  40058  atcvrj2  40207  1cvratex  40247  lplnric  40326  lplnri1  40327  lnatexN  40553  ltrnateq  40955  ltrnatneq  40956  cdleme46f2g2  41267  cdleme46f2g1  41268  dibelval1st  41923  dibelval2nd  41926  dicelval1sta  41961  hlhilphllem  42733  jm2.17b  43688  bi123impia  45199  sineq0ALT  45645  eliccre  46221  ioomidp  46230  smfinflem  47531  submodlt  48093  muldvdsfacgt  48123  iccpartiltu  48171  goldbachthlem1  48297  evengpop3  48563  gpgcubic  48844  gpg5nbgr3star  48846  itcovalsuc  49447