Theorem biimp3a 1466

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  onomeneq  9262  nn0addge1  12570  nn0addge2  12571  nn0sub2  12675  eluzp1p1  12902  uznn0sub  12913  uzinfi  12964  iocssre  13458  icossre  13459  iccssre  13460  lincmb01cmp  13526  iccf1o  13527  fzosplitprm1  13797  subfzo0  13809  modfzo0difsn  13963  hashprb  14414  pfxpfx  14716  eflt  16119  fldivndvdslt  16416  prmdiv  16787  hashgcdlem  16790  vfermltl  16803  coprimeprodsq  16810  pythagtrip  16836  difsqpwdvds  16889  cshwshashlem2  17099  odinf  19561  odcl2  19563  rnghmresel  20598  rhmresel  20627  slesolex  22675  tgtop11  22976  restntr  23177  hauscmplem  23401  icchmeo  24956  icchmeoOLD  24957  pi1xfr  25073  sinq12gt0  26535  tanord1  26564  gausslemma2dlem1a  27394  sltn0  27928  axsegconlem6  28856  lfuhgr1v0e  29190  crctcshwlkn0lem6  29749  crctcshwlkn0lem7  29750  clwlkclwwlkf1lem2  29938  s2elclwwlknon2  30037  eucrctshift  30176  eucrct2eupth  30178  nv1  30608  lnolin  30687  br8d  32530  fzm1ne1  32691  ismntd  32854  mntf  32855  cycpmco2lem6  33009  ballotlemfc0  34326  ballotlemfcc  34327  ballotlemrv2  34355  fisshasheq  34942  br8  35578  br6  35579  br4  35580  bj-imdiridlem  36892  ismtyima  37504  ismtybndlem  37507  ghomlinOLD  37589  ghomidOLD  37590  cvrcmp2  38982  atcvrj2  39132  1cvratex  39172  lplnric  39251  lplnri1  39252  lnatexN  39478  ltrnateq  39880  ltrnatneq  39881  cdleme46f2g2  40192  cdleme46f2g1  40193  dibelval1st  40848  dibelval2nd  40851  dicelval1sta  40886  hlhilphllem  41662  jm2.17b  42619  bi123impia  44165  sineq0ALT  44613  eliccre  45123  ioomidp  45132  smfinflem  46438  iccpartiltu  46994  goldbachthlem1  47117  evengpop3  47370  itcovalsuc  48055