Theorem 3expia 1232

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

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

Assertion

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

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1229	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 124	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

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

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 1007

This theorem is referenced by:  ad5ant125  1268  mp3an3  1363  3gencl  2838  moi  2990  ifnebibdc  3655  sotricim  4426  elirr  4645  en2lp  4658  suc11g  4661  3optocl  4810  sefvex  5669  f1oresrab  5820  ovmpos  6155  ov2gf  6156  poxp  6406  brtposg  6463  dfsmo2  6496  smoiun  6510  tfrlemibxssdm  6536  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  nnsucsssuc  6703  nnaordi  6719  nnawordex  6740  mapvalg  6870  pmvalg  6871  elmapg  6873  xpdom3m  7061  ordiso  7295  ctssdc  7372  pr2ne  7457  ltbtwnnqq  7695  prarloclem4  7778  addlocpr  7816  1idprl  7870  1idpru  7871  ltexprlemrnd  7885  recexprlemrnd  7909  recexprlem1ssl  7913  recexprlem1ssu  7914  recexprlemss1l  7915  recexprlemss1u  7916  aptisr  8059  axpre-apti  8165  ltxrlt  8304  axapti  8309  lttri3  8318  reapti  8818  apreap  8826  msqge0  8855  mulge0  8858  recexap  8892  mulap0b  8894  lt2msq  9125  zaddcl  9580  zdiv  9629  zextlt  9633  prime  9640  uzind2  9653  fzind  9656  lbzbi  9911  xltneg  10132  xlt2add  10176  iocssre  10249  icossre  10250  iccssre  10251  fzen  10340  rebtwn2zlemshrink  10576  qbtwnxr  10580  ioo0  10582  ioom  10583  ico0  10584  ioc0  10585  expclzaplem  10888  expnegzap  10898  expaddzap  10908  expmulzap  10910  omgadd  11128  elovmpowrd  11221  ccatopth2  11364  pfxccatin12  11380  shftuz  11457  cau3lem  11754  climuni  11933  efltim  12339  divalgb  12566  ndvdssub  12571  bitsfzo  12596  dvdsgcd  12663  lcmgcdlem  12729  qredeu  12749  isprm3  12770  prmdvdsexpr  12802  prmexpb  12803  fermltl  12886  coprimeprodsq  12910  pythagtrip  12936  pcpremul  12946  pcdvdsb  12973  pc2dvds  12983  4sqlem12  13055  4sqlem18  13061  ctinf  13131  mulgaddcom  13813  ghmrn  13924  dvdsunit  14207  unitmulclb  14209  lmodvsdi  14407  lss0cl  14465  cnntr  15036  cncnp2m  15042  cnptoprest  15050  lmtopcnp  15061  cnmptcom  15109  hmeof1o  15120  blpnf  15211  blssps  15238  blss  15239  blssec  15249  neibl  15302  climcncf  15395  cnplimcim  15478  plyadd  15562  plymul  15563  upgredg2vtx  16089  bj-peano4  16671  triap  16761