Theorem 3expia 1207

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

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

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 982

This theorem is referenced by:  ad5ant125  1243  mp3an3  1337  3gencl  2797  moi  2947  ifnebibdc  3604  sotricim  4358  elirr  4577  en2lp  4590  suc11g  4593  3optocl  4741  sefvex  5579  f1oresrab  5727  ovmpos  6046  ov2gf  6047  poxp  6290  brtposg  6312  dfsmo2  6345  smoiun  6359  tfrlemibxssdm  6385  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemaccex  6406  tfr1onlemres  6407  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemaccex  6419  tfrcllemres  6420  tfrcl  6422  nnsucsssuc  6550  nnaordi  6566  nnawordex  6587  mapvalg  6717  pmvalg  6718  elmapg  6720  xpdom3m  6893  ordiso  7102  ctssdc  7179  pr2ne  7259  ltbtwnnqq  7482  prarloclem4  7565  addlocpr  7603  1idprl  7657  1idpru  7658  ltexprlemrnd  7672  recexprlemrnd  7696  recexprlem1ssl  7700  recexprlem1ssu  7701  recexprlemss1l  7702  recexprlemss1u  7703  aptisr  7846  axpre-apti  7952  ltxrlt  8092  axapti  8097  lttri3  8106  reapti  8606  apreap  8614  msqge0  8643  mulge0  8646  recexap  8680  mulap0b  8682  lt2msq  8913  zaddcl  9366  zdiv  9414  zextlt  9418  prime  9425  uzind2  9438  fzind  9441  lbzbi  9690  xltneg  9911  xlt2add  9955  iocssre  10028  icossre  10029  iccssre  10030  fzen  10118  rebtwn2zlemshrink  10343  qbtwnxr  10347  ioo0  10349  ioom  10350  ico0  10351  ioc0  10352  expclzaplem  10655  expnegzap  10665  expaddzap  10675  expmulzap  10677  omgadd  10894  elovmpowrd  10976  shftuz  10982  cau3lem  11279  climuni  11458  efltim  11863  divalgb  12090  ndvdssub  12095  bitsfzo  12119  dvdsgcd  12179  lcmgcdlem  12245  qredeu  12265  isprm3  12286  prmdvdsexpr  12318  prmexpb  12319  fermltl  12402  coprimeprodsq  12426  pythagtrip  12452  pcpremul  12462  pcdvdsb  12489  pc2dvds  12499  4sqlem12  12571  4sqlem18  12577  ctinf  12647  mulgaddcom  13276  ghmrn  13387  dvdsunit  13668  unitmulclb  13670  lmodvsdi  13867  lss0cl  13925  cnntr  14461  cncnp2m  14467  cnptoprest  14475  lmtopcnp  14486  cnmptcom  14534  hmeof1o  14545  blpnf  14636  blssps  14663  blss  14664  blssec  14674  neibl  14727  climcncf  14820  cnplimcim  14903  plyadd  14987  plymul  14988  bj-peano4  15601  triap  15673