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  4468  elirr  4688  en2lp  4701  suc11g  4704  3optocl  4853  sefvex  5716  f1oresrab  5873  ovmpos  6212  ov2gf  6213  poxp  6468  brtposg  6525  dfsmo2  6558  smoiun  6572  tfrlemibxssdm  6598  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  nnsucsssuc  6765  nnaordi  6781  nnawordex  6802  mapvalg  6932  pmvalg  6933  elmapg  6935  xpdom3m  7132  ordiso  7376  ctssdc  7453  pr2ne  7538  ltbtwnnqq  7782  prarloclem4  7865  addlocpr  7903  1idprl  7957  1idpru  7958  ltexprlemrnd  7972  recexprlemrnd  7996  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  aptisr  8146  axpre-apti  8252  ltxrlt  8391  axapti  8396  lttri3  8405  reapti  8907  apreap  8915  msqge0  8944  mulge0  8947  recexap  8981  mulap0b  8983  lt2msq  9216  zaddcl  9684  zdiv  9734  zextlt  9738  prime  9745  uzind2  9758  fzind  9761  lbzbi  10016  xltneg  10238  xlt2add  10282  iocssre  10355  icossre  10356  iccssre  10357  fzen  10447  rebtwn2zlemshrink  10688  qbtwnxr  10692  ioo0  10694  ioom  10695  ico0  10696  ioc0  10697  expclzaplem  11000  expnegzap  11010  expaddzap  11020  expmulzap  11022  omgadd  11242  elovmpowrd  11346  ccatopth2  11489  pfxccatin12  11505  shftuz  11582  cau3lem  11880  climuni  12059  efltim  12465  divalgb  12692  ndvdssub  12697  bitsfzo  12722  dvdsgcd  12789  lcmgcdlem  12855  qredeu  12875  isprm3  12896  prmdvdsexpr  12928  prmexpb  12929  fermltl  13012  coprimeprodsq  13036  pythagtrip  13062  pcpremul  13072  pcdvdsb  13099  pc2dvds  13109  4sqlem12  13181  4sqlem18  13187  ballotfilemirc  13275  ctinf  13321  mulgaddcom  13949  ghmrn  14060  dvdsunit  14419  unitmulclb  14421  lmodvsdi  14648  lss0cl  14706  cnntr  15326  cncnp2m  15332  cnptoprest  15340  lmtopcnp  15351  cnmptcom  15399  hmeof1o  15410  blpnf  15501  blssps  15528  blss  15529  blssec  15539  neibl  15592  climcncf  15685  cnplimcim  15768  plyadd  15852  plymul  15853  upgredg2vtx  16389  lealltlt2  16752  dichmul0or  16760  bj-peano4  16981  triap  17078