Theorem 3impia 1202

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impia.1	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Assertion

Ref	Expression
3impia	|- ( ( ph /\ ps /\ ch ) -> th )

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 |- ( ( ph /\ ps ) -> ( ch -> th ) )
2	1	ex 115	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1195	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  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  mopick2  2128  3gencl  2797  mob2  2944  moi  2947  reupick3  3449  disjne  3505  disji2  4027  tz7.2  4390  funopg  5293  fvun1  5630  fvopab6  5661  isores3  5865  ovmpt4g  6049  ovmpos  6050  ov2gf  6051  ofrval  6150  poxp  6299  smoel  6367  tfr1onlemaccex  6415  tfrcllemaccex  6428  nnaass  6552  qsel  6680  xpdom3m  6902  phpm  6935  ctssdc  7188  mkvprop  7233  prarloclem3  7581  aptisr  7863  axpre-apti  7969  axapti  8114  addn0nid  8417  divvalap  8718  letrp1  8892  p1le  8893  zextle  9434  zextlt  9435  btwnnz  9437  gtndiv  9438  uzind2  9455  fzind  9458  iccleub  10023  uzsubsubfz  10139  elfz0fzfz0  10218  difelfznle  10227  elfzo0le  10278  fzonmapblen  10280  fzofzim  10281  fzosplitprm1  10327  rebtwn2zlemstep  10359  qbtwnxr  10364  icogelb  10372  expcl2lemap  10660  expclzaplem  10672  expnegzap  10682  leexp2r  10702  expnbnd  10772  bcval4  10861  bccmpl  10863  elovmpowrd  10993  absexpzap  11262  divalgb  12107  ndvdssub  12112  dvdsgcd  12204  dfgcd2  12206  rplpwr  12219  nnmindc  12226  lcmgcdlem  12270  coprmdvds1  12284  qredeq  12289  prmdvdsexpr  12343  nnnn0modprm0  12449  pcexp  12503  difsqpwdvds  12532  prmpwdvds  12549  elrestr  12949  isnmgm  13062  grpasscan1  13265  grpinvnz  13273  mulgneg2  13362  dvdsrmul1  13734  dvdsunit  13744  lmodlema  13924  mopni  14802  sincosq1lem  15145  rpcxpmul2  15233  logbgcd1irr  15287  gausslemma2dlem1a  15383  gausslemma2dlem2  15387  gausslemma2dlem4  15389  2lgsoddprmlem3  15436