Theorem biimp3a 1472

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  9150  nn0addge1  12459  nn0addge2  12460  nn0sub2  12565  eluzp1p1  12791  uznn0sub  12798  uzinfi  12853  iocssre  13355  icossre  13356  iccssre  13357  lincmb01cmp  13423  iccf1o  13424  fzosplitprm1  13706  subfzo0  13720  modfzo0difsn  13878  hashprb  14332  pfxpfx  14643  eflt  16054  fldivndvdslt  16355  prmdiv  16724  hashgcdlem  16727  vfermltl  16741  coprimeprodsq  16748  pythagtrip  16774  difsqpwdvds  16827  cshwshashlem2  17036  odinf  19504  odcl2  19506  rnghmresel  20565  rhmresel  20594  slesolex  22638  tgtop11  22938  restntr  23138  hauscmplem  23362  icchmeo  24906  icchmeoOLD  24907  pi1xfr  25023  sinq12gt0  26484  tanord1  26514  gausslemma2dlem1a  27344  ltsn0  27914  onltn0s  28366  pw2cut  28468  axsegconlem6  29007  lfuhgr1v0e  29339  crctcshwlkn0lem6  29900  crctcshwlkn0lem7  29901  clwlkclwwlkf1lem2  30092  s2elclwwlknon2  30191  eucrctshift  30330  eucrct2eupth  30332  nv1  30763  lnolin  30842  br8d  32698  fzm1ne1  32879  ismntd  33077  mntf  33078  cycpmco2lem6  33225  ballotlemfc0  34671  ballotlemfcc  34672  ballotlemrv2  34700  fisshasheq  35331  br8  35972  br6  35973  br4  35974  cgsex2gd  37392  bj-imdiridlem  37440  ismtyima  38054  ismtybndlem  38057  ghomlinOLD  38139  ghomidOLD  38140  cvrcmp2  39660  atcvrj2  39809  1cvratex  39849  lplnric  39928  lplnri1  39929  lnatexN  40155  ltrnateq  40557  ltrnatneq  40558  cdleme46f2g2  40869  cdleme46f2g1  40870  dibelval1st  41525  dibelval2nd  41528  dicelval1sta  41563  hlhilphllem  42335  jm2.17b  43318  bi123impia  44846  sineq0ALT  45292  eliccre  45865  ioomidp  45874  smfinflem  47175  submodlt  47710  iccpartiltu  47782  goldbachthlem1  47905  evengpop3  48158  gpgcubic  48439  gpg5nbgr3star  48441  itcovalsuc  49027