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  6290  tfrlemibxssdm  6385  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  nndi  6544  nnmass  6545  pr2nelem  7258  xnn0lenn0nn0  9940  difelfzle  10209  fzo1fzo0n0  10259  elfzo0z  10260  fzofzim  10264  elfzodifsumelfzo  10277  mulexp  10670  expadd  10673  expmul  10676  bernneq  10752  facdiv  10830  dvdsaddre2b  12006  addmodlteqALT  12024  ltoddhalfle  12058  halfleoddlt  12059  dfgcd2  12181  cncongr1  12271  oddprmgt2  12302  prmfac1  12320  infpnlem1  12528  dfgrp3me  13232  mulgaddcom  13276  mulginvcom  13277  fiinopn  14240  opnneissb  14391  blssps  14663  blss  14664  gausslemma2dlem1a  15299  2sqlem10  15366