Theorem biimp3a 1577

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072

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 385  df-3an 1074

This theorem is referenced by:  nn0addge1  11527  nn0addge2  11528  nn0sub2  11626  eluzp1p1  11901  uznn0sub  11908  uzinfi  11957  iocssre  12442  icossre  12443  iccssre  12444  lincmb01cmp  12504  iccf1o  12505  fzosplitprm1  12768  subfzo0  12780  modfzo0difsn  12932  hashprb  13373  swrd0fv  13635  eflt  15042  fldivndvdslt  15336  prmdiv  15688  hashgcdlem  15691  vfermltl  15704  coprimeprodsq  15711  pythagtrip  15737  difsqpwdvds  15789  cshwshashlem2  16001  odinf  18176  odcl2  18178  slesolex  20686  tgtop11  20984  restntr  21184  hauscmplem  21407  icchmeo  22937  pi1xfr  23051  sinq12gt0  24454  tanord1  24478  gausslemma2dlem1a  25285  axsegconlem6  25997  lfuhgr1v0e  26341  crctcshwlkn0lem6  26914  crctcshwlkn0lem7  26915  clwlkclwwlkf1lem2  27124  s2elclwwlknon2  27248  eucrctshift  27391  eucrct2eupth  27393  nv1  27835  lnolin  27914  br8d  29725  ballotlemfc0  30859  ballotlemfcc  30860  ballotlemrv2  30888  br8  31949  br6  31950  br4  31951  ismtyima  33911  ismtybndlem  33914  ghomlinOLD  33996  ghomidOLD  33997  cvrcmp2  35070  atcvrj2  35218  1cvratex  35258  lplnric  35337  lplnri1  35338  lnatexN  35564  ltrnateq  35967  ltrnatneq  35968  cdleme46f2g2  36279  cdleme46f2g1  36280  dibelval1st  36936  dibelval2nd  36939  dicelval1sta  36974  hlhilphllem  37749  jm2.17b  38026  bi123impia  39193  sineq0ALT  39668  eliccre  40227  ioomidp  40239  smfinflem  41525  iccpartiltu  41864  pfxpfx  41921  repswpfx  41942  goldbachthlem1  41963  evengpop3  42192  rnghmresel  42470  rhmresel  42516