Theorem 3imp 1219

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

Hypothesis

Ref	Expression
3imp.1	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
3imp	|- ( ( ph /\ ps /\ ch ) -> th )

Proof of Theorem 3imp

Step	Hyp	Ref	Expression
1		df-3an 1006	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		3imp.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 256	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	sylbi 121	1 |- ( ( ph /\ ps /\ ch ) -> th )

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  11269  swrdswrdlem  11289  pfxccat3  11319  reuccatpfxs1lem  11331  dvdsaddre2b  12407  addmodlteqALT  12425  ltoddhalfle  12459  halfleoddlt  12460  dfgcd2  12590  cncongr1  12680  oddprmgt2  12711  prmfac1  12729  infpnlem1  12937  dfgrp3me  13688  mulgaddcom  13738  mulginvcom  13739  fiinopn  14734  opnneissb  14885  blssps  15157  blss  15158  gausslemma2dlem1a  15793  2sqlem10  15860  ausgrumgrien  16027  ausgrusgrien  16028  ushgredgedg  16083  ushgredgedgloop  16085  edg0usgr  16104  0uhgrsubgr  16122  subumgredg2en  16128  wlkl1loop  16215  clwwlkccatlem  16257  umgrclwwlkge2  16259  clwwlkn1loopb  16277  clwwlkext2edg  16279  clwwlknonex2lem2  16295  clwwlknonex2  16296  clwwlknonex2e  16297  eupth2lem3lem6fi  16328