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  6235  tfrlemibxssdm  6330  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  nndi  6489  nnmass  6490  pr2nelem  7192  xnn0lenn0nn0  9867  difelfzle  10136  fzo1fzo0n0  10185  elfzo0z  10186  fzofzim  10190  elfzodifsumelfzo  10203  mulexp  10561  expadd  10564  expmul  10567  bernneq  10643  facdiv  10720  dvdsaddre2b  11850  addmodlteqALT  11867  ltoddhalfle  11900  halfleoddlt  11901  dfgcd2  12017  cncongr1  12105  oddprmgt2  12136  prmfac1  12154  infpnlem1  12359  dfgrp3me  12975  mulgaddcom  13012  mulginvcom  13013  fiinopn  13543  opnneissb  13694  blssps  13966  blss  13967  2sqlem10  14511