Theorem biimp3a 1424

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031

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

This theorem is referenced by:  nn0addge1  11216  nn0addge2  11217  nn0sub2  11315  eluzp1p1  11589  uznn0sub  11595  uzinfi  11644  iocssre  12124  icossre  12125  iccssre  12126  lincmb01cmp  12186  iccf1o  12187  fzosplitprm1  12443  subfzo0  12452  modfzo0difsn  12604  hashprb  13046  swrd0fv  13291  eflt  14686  fldivndvdslt  14976  prmdiv  15328  hashgcdlem  15331  vfermltl  15344  coprimeprodsq  15351  pythagtrip  15377  difsqpwdvds  15429  cshwshashlem2  15641  odinf  17803  odcl2  17805  slesolex  20307  tgtop11  20597  restntr  20796  hauscmplem  21019  icchmeo  22548  pi1xfr  22663  sinq12gt0  24063  tanord1  24087  gausslemma2dlem1a  24890  axsegconlem6  25602  nv1  26914  lnolin  26993  br8d  28802  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemrv2  29910  br8  30899  br6  30900  br4  30901  ismtyima  32772  ismtybndlem  32775  ghomlinOLD  32857  ghomidOLD  32858  cvrcmp2  33589  atcvrj2  33737  1cvratex  33777  lplnric  33856  lplnri1  33857  lnatexN  34083  ltrnateq  34486  ltrnatneq  34487  cdleme46f2g2  34799  cdleme46f2g1  34800  dibelval1st  35456  dibelval2nd  35459  dicelval1sta  35494  hlhilphllem  36269  jm2.17b  36546  bi123impia  37716  sineq0ALT  38195  eliccre  38575  ioomidp  38587  iccpartiltu  39960  goldbachthlem1  39995  fmtnoprmfac1lem  40014  evengpop3  40214  pfxpfx  40278  repswpfx  40299  lfuhgr1v0e  40480  crctcsh1wlkn0lem6  41018  crctcsh1wlkn0lem7  41019  eucrctshift  41411  eucrct2eupth  41413  rnghmresel  41756  rhmresel  41802