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  9237  nn0addge1  12547  nn0addge2  12548  nn0sub2  12654  eluzp1p1  12880  uznn0sub  12891  uzinfi  12944  iocssre  13444  icossre  13445  iccssre  13446  lincmb01cmp  13512  iccf1o  13513  fzosplitprm1  13793  subfzo0  13805  modfzo0difsn  13961  hashprb  14415  pfxpfx  14726  eflt  16135  fldivndvdslt  16435  prmdiv  16804  hashgcdlem  16807  vfermltl  16821  coprimeprodsq  16828  pythagtrip  16854  difsqpwdvds  16907  cshwshashlem2  17116  odinf  19544  odcl2  19546  rnghmresel  20580  rhmresel  20609  slesolex  22620  tgtop11  22920  restntr  23120  hauscmplem  23344  icchmeo  24889  icchmeoOLD  24890  pi1xfr  25006  sinq12gt0  26468  tanord1  26498  gausslemma2dlem1a  27328  sltn0  27869  onltn0s  28300  pw2cut  28387  axsegconlem6  28901  lfuhgr1v0e  29233  crctcshwlkn0lem6  29797  crctcshwlkn0lem7  29798  clwlkclwwlkf1lem2  29986  s2elclwwlknon2  30085  eucrctshift  30224  eucrct2eupth  30226  nv1  30656  lnolin  30735  br8d  32590  fzm1ne1  32765  ismntd  32964  mntf  32965  cycpmco2lem6  33142  ballotlemfc0  34525  ballotlemfcc  34526  ballotlemrv2  34554  fisshasheq  35137  br8  35773  br6  35774  br4  35775  bj-imdiridlem  37203  ismtyima  37827  ismtybndlem  37830  ghomlinOLD  37912  ghomidOLD  37913  cvrcmp2  39302  atcvrj2  39452  1cvratex  39492  lplnric  39571  lplnri1  39572  lnatexN  39798  ltrnateq  40200  ltrnatneq  40201  cdleme46f2g2  40512  cdleme46f2g1  40513  dibelval1st  41168  dibelval2nd  41171  dicelval1sta  41206  hlhilphllem  41978  jm2.17b  42985  bi123impia  44515  sineq0ALT  44961  eliccre  45534  ioomidp  45543  smfinflem  46846  submodlt  47379  iccpartiltu  47436  goldbachthlem1  47559  evengpop3  47812  gpgcubic  48081  gpg5nbgr3star  48083  itcovalsuc  48647