Theorem 3expia 1236

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 1233	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 124	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ad5ant125  1272  mp3an3  1367  3gencl  2856  moi  3009  ifnebibdc  3686  sotricim  4470  elirr  4690  en2lp  4703  suc11g  4706  3optocl  4855  sefvex  5719  f1oresrab  5876  ovmpos  6215  ov2gf  6216  poxp  6472  brtposg  6530  dfsmo2  6563  smoiun  6577  tfrlemibxssdm  6603  tfr1onlemsucfn  6616  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemaccex  6637  tfrcllemres  6638  tfrcl  6640  nnsucsssuc  6770  nnaordi  6786  nnawordex  6807  mapvalg  6937  pmvalg  6938  elmapg  6940  xpdom3m  7138  ordiso  7382  ctssdc  7459  pr2ne  7544  ltbtwnnqq  7788  prarloclem4  7871  addlocpr  7909  1idprl  7963  1idpru  7964  ltexprlemrnd  7978  recexprlemrnd  8002  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  aptisr  8152  axpre-apti  8258  ltxrlt  8397  axapti  8402  lttri3  8411  reapti  8915  apreap  8923  msqge0  8952  mulge0  8955  recexap  8989  mulap0b  8991  lt2msq  9224  zaddcl  9693  zdiv  9744  zextlt  9748  prime  9755  uzind2  9768  fzind  9771  lbzbi  10031  xltneg  10254  xlt2add  10298  iocssre  10371  icossre  10372  iccssre  10373  fzen  10463  rebtwn2zlemshrink  10704  qbtwnxr  10708  ioo0  10710  ioom  10711  ico0  10712  ioc0  10713  expclzaplem  11020  expnegzap  11030  expaddzap  11040  expmulzap  11042  omgadd  11263  elovmpowrd  11367  ccatopth2  11510  pfxccatin12  11526  shftuz  11603  cau3lem  11902  climuni  12083  efltim  12489  divalgb  12716  ndvdssub  12721  bitsfzo  12746  dvdsgcd  12813  lcmgcdlem  12879  qredeu  12899  isprm3  12920  prmdvdsexpr  12953  prmexpb  12954  fermltl  13040  coprimeprodsq  13064  pythagtrip  13090  pcpremul  13100  pcdvdsb  13127  pc2dvds  13137  4sqlem12  13209  4sqlem18  13215  ballotfilemirc  13332  ctinf  13378  mulgaddcom  14007  ghmrn  14118  gsumcom2fi  14274  dvdsunit  14527  unitmulclb  14529  lmodvsdi  14756  lss0cl  14814  mvrf1fi  15219  cnntr  15468  cncnp2m  15474  cnptoprest  15482  lmtopcnp  15493  cnmptcom  15541  hmeof1o  15552  blpnf  15643  blssps  15670  blss  15671  blssec  15681  neibl  15734  climcncf  15827  cnplimcim  15910  plyadd  15994  plymul  15995  rpcxpmul2z  16165  chtublem  16312  bposlem3  16330  upgredg2vtx  16611  lealltlt2  16974  dichmul0or  16982  bj-peano4  17203  triap  17301