Theorem 3impia 1203

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 1196	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981

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 983

This theorem is referenced by:  mopick2  2137  3gencl  2806  mob2  2953  moi  2956  reupick3  3458  disjne  3514  disji2  4037  tz7.2  4402  funopg  5306  fvun1  5647  fvopab6  5678  isores3  5886  ovmpt4g  6070  ovmpos  6071  ov2gf  6072  ofrval  6171  poxp  6320  smoel  6388  tfr1onlemaccex  6436  tfrcllemaccex  6449  nnaass  6573  qsel  6701  xpdom3m  6931  phpm  6964  ctssdc  7217  mkvprop  7262  prarloclem3  7612  aptisr  7894  axpre-apti  8000  axapti  8145  addn0nid  8448  divvalap  8749  letrp1  8923  p1le  8924  zextle  9466  zextlt  9467  btwnnz  9469  gtndiv  9470  uzind2  9487  fzind  9490  iccleub  10055  uzsubsubfz  10171  elfz0fzfz0  10250  difelfznle  10259  elfzo0le  10311  fzonmapblen  10313  fzofzim  10314  fzosplitprm1  10365  rebtwn2zlemstep  10397  qbtwnxr  10402  icogelb  10410  expcl2lemap  10698  expclzaplem  10710  expnegzap  10720  leexp2r  10740  expnbnd  10810  bcval4  10899  bccmpl  10901  elovmpowrd  11037  ccatval2  11057  wrdl1s1  11087  swrdsb0eq  11121  absexpzap  11424  divalgb  12269  ndvdssub  12274  dvdsgcd  12366  dfgcd2  12368  rplpwr  12381  nnmindc  12388  lcmgcdlem  12432  coprmdvds1  12446  qredeq  12451  prmdvdsexpr  12505  nnnn0modprm0  12611  pcexp  12665  difsqpwdvds  12694  prmpwdvds  12711  elrestr  13112  isnmgm  13225  grpasscan1  13428  grpinvnz  13436  mulgneg2  13525  dvdsrmul1  13897  dvdsunit  13907  lmodlema  14087  mopni  14987  sincosq1lem  15330  rpcxpmul2  15418  logbgcd1irr  15472  gausslemma2dlem1a  15568  gausslemma2dlem2  15572  gausslemma2dlem4  15574  2lgsoddprmlem3  15621