Theorem biimp3a 1470

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  onomeneq  9228  nn0addge1  12518  nn0addge2  12519  nn0sub2  12623  eluzp1p1  12850  uznn0sub  12861  uzinfi  12912  iocssre  13404  icossre  13405  iccssre  13406  lincmb01cmp  13472  iccf1o  13473  fzosplitprm1  13742  subfzo0  13754  modfzo0difsn  13908  hashprb  14357  pfxpfx  14658  eflt  16060  fldivndvdslt  16357  prmdiv  16718  hashgcdlem  16721  vfermltl  16734  coprimeprodsq  16741  pythagtrip  16767  difsqpwdvds  16820  cshwshashlem2  17030  odinf  19431  odcl2  19433  slesolex  22184  tgtop11  22485  restntr  22686  hauscmplem  22910  icchmeo  24457  pi1xfr  24571  sinq12gt0  26017  tanord1  26046  gausslemma2dlem1a  26868  sltn0  27399  axsegconlem6  28180  lfuhgr1v0e  28511  crctcshwlkn0lem6  29069  crctcshwlkn0lem7  29070  clwlkclwwlkf1lem2  29258  s2elclwwlknon2  29357  eucrctshift  29496  eucrct2eupth  29498  nv1  29928  lnolin  30007  br8d  31839  fzm1ne1  32000  ismntd  32154  mntf  32155  cycpmco2lem6  32290  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemrv2  33520  fisshasheq  34104  br8  34726  br6  34727  br4  34728  gg-icchmeo  35170  bj-imdiridlem  36066  ismtyima  36671  ismtybndlem  36674  ghomlinOLD  36756  ghomidOLD  36757  cvrcmp2  38154  atcvrj2  38304  1cvratex  38344  lplnric  38423  lplnri1  38424  lnatexN  38650  ltrnateq  39052  ltrnatneq  39053  cdleme46f2g2  39364  cdleme46f2g1  39365  dibelval1st  40020  dibelval2nd  40023  dicelval1sta  40058  hlhilphllem  40834  jm2.17b  41700  bi123impia  43250  sineq0ALT  43698  eliccre  44218  ioomidp  44227  smfinflem  45533  iccpartiltu  46090  goldbachthlem1  46213  evengpop3  46466  rnghmresel  46862  rhmresel  46908  itcovalsuc  47353