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  2794  moi  2944  ifnebibdc  3601  sotricim  4355  elirr  4574  en2lp  4587  suc11g  4590  3optocl  4738  sefvex  5576  f1oresrab  5724  ovmpos  6043  ov2gf  6044  poxp  6287  brtposg  6309  dfsmo2  6342  smoiun  6356  tfrlemibxssdm  6382  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemaccex  6403  tfr1onlemres  6404  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemaccex  6416  tfrcllemres  6417  tfrcl  6419  nnsucsssuc  6547  nnaordi  6563  nnawordex  6584  mapvalg  6714  pmvalg  6715  elmapg  6717  xpdom3m  6890  ordiso  7097  ctssdc  7174  pr2ne  7254  ltbtwnnqq  7477  prarloclem4  7560  addlocpr  7598  1idprl  7652  1idpru  7653  ltexprlemrnd  7667  recexprlemrnd  7691  recexprlem1ssl  7695  recexprlem1ssu  7696  recexprlemss1l  7697  recexprlemss1u  7698  aptisr  7841  axpre-apti  7947  ltxrlt  8087  axapti  8092  lttri3  8101  reapti  8600  apreap  8608  msqge0  8637  mulge0  8640  recexap  8674  mulap0b  8676  lt2msq  8907  zaddcl  9360  zdiv  9408  zextlt  9412  prime  9419  uzind2  9432  fzind  9435  lbzbi  9684  xltneg  9905  xlt2add  9949  iocssre  10022  icossre  10023  iccssre  10024  fzen  10112  rebtwn2zlemshrink  10325  qbtwnxr  10329  ioo0  10331  ioom  10332  ico0  10333  ioc0  10334  expclzaplem  10637  expnegzap  10647  expaddzap  10657  expmulzap  10659  omgadd  10876  elovmpowrd  10958  shftuz  10964  cau3lem  11261  climuni  11439  efltim  11844  divalgb  12069  ndvdssub  12074  dvdsgcd  12152  lcmgcdlem  12218  qredeu  12238  isprm3  12259  prmdvdsexpr  12291  prmexpb  12292  fermltl  12375  coprimeprodsq  12398  pythagtrip  12424  pcpremul  12434  pcdvdsb  12461  pc2dvds  12471  4sqlem12  12543  4sqlem18  12549  ctinf  12590  mulgaddcom  13219  ghmrn  13330  dvdsunit  13611  unitmulclb  13613  lmodvsdi  13810  lss0cl  13868  cnntr  14404  cncnp2m  14410  cnptoprest  14418  lmtopcnp  14429  cnmptcom  14477  hmeof1o  14488  blpnf  14579  blssps  14606  blss  14607  blssec  14617  neibl  14670  climcncf  14763  cnplimcim  14846  plyadd  14930  plymul  14931  bj-peano4  15517  triap  15589