Theorem 3imp 1195

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 982	. 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 980

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 982

This theorem is referenced by:  3impa  1196  3imp31  1198  3imp231  1199  3impb  1201  3impia  1202  3impib  1203  3com23  1211  3an1rs  1221  3imp1  1222  3impd  1223  syl3an2  1283  syl3an3  1284  3jao  1312  biimp3ar  1357  poxp  6285  tfrlemibxssdm  6380  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  nndi  6539  nnmass  6540  pr2nelem  7251  xnn0lenn0nn0  9931  difelfzle  10200  fzo1fzo0n0  10250  elfzo0z  10251  fzofzim  10255  elfzodifsumelfzo  10268  mulexp  10649  expadd  10652  expmul  10655  bernneq  10731  facdiv  10809  dvdsaddre2b  11984  addmodlteqALT  12001  ltoddhalfle  12034  halfleoddlt  12035  dfgcd2  12151  cncongr1  12241  oddprmgt2  12272  prmfac1  12290  infpnlem1  12497  dfgrp3me  13172  mulgaddcom  13216  mulginvcom  13217  fiinopn  14172  opnneissb  14323  blssps  14595  blss  14596  gausslemma2dlem1a  15174  2sqlem10  15212