Theorem biimp3a 1429

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  nn0addge1  11283  nn0addge2  11284  nn0sub2  11382  eluzp1p1  11657  uznn0sub  11663  uzinfi  11712  iocssre  12195  icossre  12196  iccssre  12197  lincmb01cmp  12257  iccf1o  12258  fzosplitprm1  12518  subfzo0  12530  modfzo0difsn  12682  hashprb  13125  swrd0fv  13377  eflt  14772  fldivndvdslt  15062  prmdiv  15414  hashgcdlem  15417  vfermltl  15430  coprimeprodsq  15437  pythagtrip  15463  difsqpwdvds  15515  cshwshashlem2  15727  odinf  17901  odcl2  17903  slesolex  20407  tgtop11  20697  restntr  20896  hauscmplem  21119  icchmeo  22648  pi1xfr  22763  sinq12gt0  24163  tanord1  24187  gausslemma2dlem1a  24990  axsegconlem6  25702  lfuhgr1v0e  26039  crctcshwlkn0lem6  26576  crctcshwlkn0lem7  26577  eucrctshift  26969  eucrct2eupth  26971  nv1  27376  lnolin  27455  br8d  29262  ballotlemfc0  30332  ballotlemfcc  30333  ballotlemrv2  30361  br8  31351  br6  31352  br4  31353  ismtyima  33231  ismtybndlem  33234  ghomlinOLD  33316  ghomidOLD  33317  cvrcmp2  34048  atcvrj2  34196  1cvratex  34236  lplnric  34315  lplnri1  34316  lnatexN  34542  ltrnateq  34945  ltrnatneq  34946  cdleme46f2g2  35258  cdleme46f2g1  35259  dibelval1st  35915  dibelval2nd  35918  dicelval1sta  35953  hlhilphllem  36728  jm2.17b  37005  bi123impia  38174  sineq0ALT  38653  eliccre  39136  ioomidp  39148  smfinflem  40327  iccpartiltu  40653  pfxpfx  40711  repswpfx  40732  goldbachthlem1  40753  fmtnoprmfac1lem  40772  evengpop3  40972  rnghmresel  41249  rhmresel  41295