Theorem 3imp 1219

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 1006	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3imp.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 256	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	sylbi 121	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1006

This theorem is referenced by:  3impa  1220  3imp31  1222  3imp231  1223  3impb  1225  3impia  1226  3impib  1227  3com23  1235  3an1rs  1245  3imp1  1246  3impd  1247  syl3an2  1307  syl3an3  1308  3jao  1337  biimp3ar  1382  f1ssf1  5615  poxp  6397  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  nndi  6654  nnmass  6655  pr2nelem  7396  xnn0lenn0nn0  10100  difelfzle  10369  fzo1fzo0n0  10423  elfzo0z  10424  fzofzim  10428  elfzodifsumelfzo  10447  mulexp  10841  expadd  10844  expmul  10847  bernneq  10923  facdiv  11001  pfxfv  11266  swrdswrdlem  11286  pfxccat3  11316  reuccatpfxs1lem  11328  dvdsaddre2b  12404  addmodlteqALT  12422  ltoddhalfle  12456  halfleoddlt  12457  dfgcd2  12587  cncongr1  12677  oddprmgt2  12708  prmfac1  12726  infpnlem1  12934  dfgrp3me  13685  mulgaddcom  13735  mulginvcom  13736  fiinopn  14731  opnneissb  14882  blssps  15154  blss  15155  gausslemma2dlem1a  15790  2sqlem10  15857  ausgrumgrien  16024  ausgrusgrien  16025  ushgredgedg  16080  ushgredgedgloop  16082  edg0usgr  16101  0uhgrsubgr  16119  subumgredg2en  16125  wlkl1loop  16212  clwwlkccatlem  16254  umgrclwwlkge2  16256  clwwlkn1loopb  16274  clwwlkext2edg  16276  clwwlknonex2lem2  16292  clwwlknonex2  16293  clwwlknonex2e  16294  eupth2lem3lem6fi  16325