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  4401  funopg  5305  fvun1  5645  fvopab6  5676  isores3  5884  ovmpt4g  6068  ovmpos  6069  ov2gf  6070  ofrval  6169  poxp  6318  smoel  6386  tfr1onlemaccex  6434  tfrcllemaccex  6447  nnaass  6571  qsel  6699  xpdom3m  6929  phpm  6962  ctssdc  7215  mkvprop  7260  prarloclem3  7610  aptisr  7892  axpre-apti  7998  axapti  8143  addn0nid  8446  divvalap  8747  letrp1  8921  p1le  8922  zextle  9464  zextlt  9465  btwnnz  9467  gtndiv  9468  uzind2  9485  fzind  9488  iccleub  10053  uzsubsubfz  10169  elfz0fzfz0  10248  difelfznle  10257  elfzo0le  10309  fzonmapblen  10311  fzofzim  10312  fzosplitprm1  10363  rebtwn2zlemstep  10395  qbtwnxr  10400  icogelb  10408  expcl2lemap  10696  expclzaplem  10708  expnegzap  10718  leexp2r  10738  expnbnd  10808  bcval4  10897  bccmpl  10899  elovmpowrd  11035  ccatval2  11054  wrdl1s1  11084  swrdsb0eq  11118  absexpzap  11391  divalgb  12236  ndvdssub  12241  dvdsgcd  12333  dfgcd2  12335  rplpwr  12348  nnmindc  12355  lcmgcdlem  12399  coprmdvds1  12413  qredeq  12418  prmdvdsexpr  12472  nnnn0modprm0  12578  pcexp  12632  difsqpwdvds  12661  prmpwdvds  12678  elrestr  13079  isnmgm  13192  grpasscan1  13395  grpinvnz  13403  mulgneg2  13492  dvdsrmul1  13864  dvdsunit  13874  lmodlema  14054  mopni  14954  sincosq1lem  15297  rpcxpmul2  15385  logbgcd1irr  15439  gausslemma2dlem1a  15535  gausslemma2dlem2  15539  gausslemma2dlem4  15541  2lgsoddprmlem3  15588