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

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

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 1088

This theorem is referenced by:  onomeneq  9155  nn0addge1  12464  nn0addge2  12465  nn0sub2  12571  eluzp1p1  12797  uznn0sub  12808  uzinfi  12863  iocssre  13364  icossre  13365  iccssre  13366  lincmb01cmp  13432  iccf1o  13433  fzosplitprm1  13714  subfzo0  13726  modfzo0difsn  13884  hashprb  14338  pfxpfx  14649  eflt  16061  fldivndvdslt  16362  prmdiv  16731  hashgcdlem  16734  vfermltl  16748  coprimeprodsq  16755  pythagtrip  16781  difsqpwdvds  16834  cshwshashlem2  17043  odinf  19469  odcl2  19471  rnghmresel  20505  rhmresel  20534  slesolex  22545  tgtop11  22845  restntr  23045  hauscmplem  23269  icchmeo  24814  icchmeoOLD  24815  pi1xfr  24931  sinq12gt0  26392  tanord1  26422  gausslemma2dlem1a  27252  sltn0  27793  onltn0s  28224  pw2cut  28311  axsegconlem6  28825  lfuhgr1v0e  29157  crctcshwlkn0lem6  29718  crctcshwlkn0lem7  29719  clwlkclwwlkf1lem2  29907  s2elclwwlknon2  30006  eucrctshift  30145  eucrct2eupth  30147  nv1  30577  lnolin  30656  br8d  32511  fzm1ne1  32684  ismntd  32883  mntf  32884  cycpmco2lem6  33061  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemrv2  34486  fisshasheq  35075  br8  35716  br6  35717  br4  35718  bj-imdiridlem  37146  ismtyima  37770  ismtybndlem  37773  ghomlinOLD  37855  ghomidOLD  37856  cvrcmp2  39250  atcvrj2  39400  1cvratex  39440  lplnric  39519  lplnri1  39520  lnatexN  39746  ltrnateq  40148  ltrnatneq  40149  cdleme46f2g2  40460  cdleme46f2g1  40461  dibelval1st  41116  dibelval2nd  41119  dicelval1sta  41154  hlhilphllem  41926  jm2.17b  42923  bi123impia  44453  sineq0ALT  44899  eliccre  45476  ioomidp  45485  smfinflem  46788  submodlt  47324  iccpartiltu  47396  goldbachthlem1  47519  evengpop3  47772  gpgcubic  48043  gpg5nbgr3star  48045  itcovalsuc  48629