Theorem biimp3a 1471

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  onomeneq  9265  nn0addge1  12572  nn0addge2  12573  nn0sub2  12679  eluzp1p1  12906  uznn0sub  12917  uzinfi  12970  iocssre  13467  icossre  13468  iccssre  13469  lincmb01cmp  13535  iccf1o  13536  fzosplitprm1  13816  subfzo0  13828  modfzo0difsn  13984  hashprb  14436  pfxpfx  14746  eflt  16153  fldivndvdslt  16453  prmdiv  16822  hashgcdlem  16825  vfermltl  16839  coprimeprodsq  16846  pythagtrip  16872  difsqpwdvds  16925  cshwshashlem2  17134  odinf  19581  odcl2  19583  rnghmresel  20620  rhmresel  20649  slesolex  22688  tgtop11  22989  restntr  23190  hauscmplem  23414  icchmeo  24971  icchmeoOLD  24972  pi1xfr  25088  sinq12gt0  26549  tanord1  26579  gausslemma2dlem1a  27409  sltn0  27943  pw2cut  28420  axsegconlem6  28937  lfuhgr1v0e  29271  crctcshwlkn0lem6  29835  crctcshwlkn0lem7  29836  clwlkclwwlkf1lem2  30024  s2elclwwlknon2  30123  eucrctshift  30262  eucrct2eupth  30264  nv1  30694  lnolin  30773  br8d  32622  fzm1ne1  32790  ismntd  32974  mntf  32975  cycpmco2lem6  33151  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemrv2  34524  fisshasheq  35120  br8  35756  br6  35757  br4  35758  bj-imdiridlem  37186  ismtyima  37810  ismtybndlem  37813  ghomlinOLD  37895  ghomidOLD  37896  cvrcmp2  39285  atcvrj2  39435  1cvratex  39475  lplnric  39554  lplnri1  39555  lnatexN  39781  ltrnateq  40183  ltrnatneq  40184  cdleme46f2g2  40495  cdleme46f2g1  40496  dibelval1st  41151  dibelval2nd  41154  dicelval1sta  41189  hlhilphllem  41965  jm2.17b  42973  bi123impia  44510  sineq0ALT  44957  eliccre  45518  ioomidp  45527  smfinflem  46832  submodlt  47352  iccpartiltu  47409  goldbachthlem1  47532  evengpop3  47785  gpgcubic  48035  gpg5nbgr3star  48037  itcovalsuc  48588