Theorem 3imp 1193

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

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 980

This theorem is referenced by:  3impa  1194  3imp31  1196  3imp231  1197  3impb  1199  3impia  1200  3impib  1201  3com23  1209  3an1rs  1219  3imp1  1220  3impd  1221  syl3an2  1272  syl3an3  1273  3jao  1301  biimp3ar  1346  poxp  6230  tfrlemibxssdm  6325  tfr1onlembxssdm  6341  tfrcllembxssdm  6354  nndi  6484  nnmass  6485  pr2nelem  7187  xnn0lenn0nn0  9861  difelfzle  10129  fzo1fzo0n0  10178  elfzo0z  10179  fzofzim  10183  elfzodifsumelfzo  10196  mulexp  10554  expadd  10557  expmul  10560  bernneq  10635  facdiv  10711  addmodlteqALT  11857  ltoddhalfle  11890  halfleoddlt  11891  dfgcd2  12007  cncongr1  12095  oddprmgt2  12126  prmfac1  12144  infpnlem1  12349  dfgrp3me  12902  mulgaddcom  12938  mulginvcom  12939  fiinopn  13373  opnneissb  13526  blssps  13798  blss  13799  2sqlem10  14332