Theorem biimp3a 1469

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  9291  nn0addge1  12599  nn0addge2  12600  nn0sub2  12704  eluzp1p1  12931  uznn0sub  12942  uzinfi  12993  iocssre  13487  icossre  13488  iccssre  13489  lincmb01cmp  13555  iccf1o  13556  fzosplitprm1  13827  subfzo0  13839  modfzo0difsn  13994  hashprb  14446  pfxpfx  14756  eflt  16165  fldivndvdslt  16462  prmdiv  16832  hashgcdlem  16835  vfermltl  16848  coprimeprodsq  16855  pythagtrip  16881  difsqpwdvds  16934  cshwshashlem2  17144  odinf  19605  odcl2  19607  rnghmresel  20642  rhmresel  20671  slesolex  22709  tgtop11  23010  restntr  23211  hauscmplem  23435  icchmeo  24990  icchmeoOLD  24991  pi1xfr  25107  sinq12gt0  26567  tanord1  26597  gausslemma2dlem1a  27427  sltn0  27961  pw2cut  28438  axsegconlem6  28955  lfuhgr1v0e  29289  crctcshwlkn0lem6  29848  crctcshwlkn0lem7  29849  clwlkclwwlkf1lem2  30037  s2elclwwlknon2  30136  eucrctshift  30275  eucrct2eupth  30277  nv1  30707  lnolin  30786  br8d  32632  fzm1ne1  32794  ismntd  32957  mntf  32958  cycpmco2lem6  33124  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemrv2  34486  fisshasheq  35082  br8  35718  br6  35719  br4  35720  bj-imdiridlem  37151  ismtyima  37763  ismtybndlem  37766  ghomlinOLD  37848  ghomidOLD  37849  cvrcmp2  39240  atcvrj2  39390  1cvratex  39430  lplnric  39509  lplnri1  39510  lnatexN  39736  ltrnateq  40138  ltrnatneq  40139  cdleme46f2g2  40450  cdleme46f2g1  40451  dibelval1st  41106  dibelval2nd  41109  dicelval1sta  41144  hlhilphllem  41920  jm2.17b  42918  bi123impia  44460  sineq0ALT  44908  eliccre  45423  ioomidp  45432  smfinflem  46738  iccpartiltu  47296  goldbachthlem1  47419  evengpop3  47672  itcovalsuc  48401