Theorem 3imp 1217

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 1004	. 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 1002

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 1004

This theorem is referenced by:  3impa  1218  3imp31  1220  3imp231  1221  3impb  1223  3impia  1224  3impib  1225  3com23  1233  3an1rs  1243  3imp1  1244  3impd  1245  syl3an2  1305  syl3an3  1306  3jao  1335  biimp3ar  1380  poxp  6392  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  nndi  6649  nnmass  6650  pr2nelem  7387  xnn0lenn0nn0  10090  difelfzle  10359  fzo1fzo0n0  10412  elfzo0z  10413  fzofzim  10417  elfzodifsumelfzo  10436  mulexp  10830  expadd  10833  expmul  10836  bernneq  10912  facdiv  10990  pfxfv  11255  swrdswrdlem  11275  pfxccat3  11305  reuccatpfxs1lem  11317  dvdsaddre2b  12392  addmodlteqALT  12410  ltoddhalfle  12444  halfleoddlt  12445  dfgcd2  12575  cncongr1  12665  oddprmgt2  12696  prmfac1  12714  infpnlem1  12922  dfgrp3me  13673  mulgaddcom  13723  mulginvcom  13724  fiinopn  14718  opnneissb  14869  blssps  15141  blss  15142  gausslemma2dlem1a  15777  2sqlem10  15844  ausgrumgrien  16009  ausgrusgrien  16010  ushgredgedg  16065  ushgredgedgloop  16067  edg0usgr  16086  wlkl1loop  16155  clwwlkccatlem  16195  umgrclwwlkge2  16197  clwwlkn1loopb  16215  clwwlkext2edg  16217  clwwlknonex2lem2  16233  clwwlknonex2  16234  clwwlknonex2e  16235