Theorem 3imp 1217

Description: Importation inference. (Contributed by NM, 8-Apr-1994.)

Hypothesis

Ref	Expression
3imp.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
3imp	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3imp

Step	Hyp	Ref	Expression
1		df-3an 1004	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3imp.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 256	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	sylbi 121	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  3impa  1218  3imp31  1220  3imp231  1221  3impb  1223  3impia  1224  3impib  1225  3com23  1233  3an1rs  1243  3imp1  1244  3impd  1245  syl3an2  1305  syl3an3  1306  3jao  1335  biimp3ar  1380  poxp  6392  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  nndi  6649  nnmass  6650  pr2nelem  7390  xnn0lenn0nn0  10093  difelfzle  10362  fzo1fzo0n0  10415  elfzo0z  10416  fzofzim  10420  elfzodifsumelfzo  10439  mulexp  10833  expadd  10836  expmul  10839  bernneq  10915  facdiv  10993  pfxfv  11258  swrdswrdlem  11278  pfxccat3  11308  reuccatpfxs1lem  11320  dvdsaddre2b  12395  addmodlteqALT  12413  ltoddhalfle  12447  halfleoddlt  12448  dfgcd2  12578  cncongr1  12668  oddprmgt2  12699  prmfac1  12717  infpnlem1  12925  dfgrp3me  13676  mulgaddcom  13726  mulginvcom  13727  fiinopn  14721  opnneissb  14872  blssps  15144  blss  15145  gausslemma2dlem1a  15780  2sqlem10  15847  ausgrumgrien  16014  ausgrusgrien  16015  ushgredgedg  16070  ushgredgedgloop  16072  edg0usgr  16091  wlkl1loop  16169  clwwlkccatlem  16209  umgrclwwlkge2  16211  clwwlkn1loopb  16229  clwwlkext2edg  16231  clwwlknonex2lem2  16247  clwwlknonex2  16248  clwwlknonex2e  16249