Theorem 3expia 1200

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  mp3an3  1321  3gencl  2764  moi  2913  sotricim  4308  elirr  4525  en2lp  4538  suc11g  4541  3optocl  4689  sefvex  5517  f1oresrab  5661  ovmpos  5976  ov2gf  5977  poxp  6211  brtposg  6233  dfsmo2  6266  smoiun  6280  tfrlemibxssdm  6306  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemaccex  6340  tfrcllemres  6341  tfrcl  6343  nnsucsssuc  6471  nnaordi  6487  nnawordex  6508  mapvalg  6636  pmvalg  6637  elmapg  6639  xpdom3m  6812  ordiso  7013  ctssdc  7090  pr2ne  7169  ltbtwnnqq  7377  prarloclem4  7460  addlocpr  7498  1idprl  7552  1idpru  7553  ltexprlemrnd  7567  recexprlemrnd  7591  recexprlem1ssl  7595  recexprlem1ssu  7596  recexprlemss1l  7597  recexprlemss1u  7598  aptisr  7741  axpre-apti  7847  ltxrlt  7985  axapti  7990  lttri3  7999  reapti  8498  apreap  8506  msqge0  8535  mulge0  8538  recexap  8571  mulap0b  8573  lt2msq  8802  zaddcl  9252  zdiv  9300  zextlt  9304  prime  9311  uzind2  9324  fzind  9327  lbzbi  9575  xltneg  9793  xlt2add  9837  iocssre  9910  icossre  9911  iccssre  9912  fzen  9999  rebtwn2zlemshrink  10210  qbtwnxr  10214  ioo0  10216  ioom  10217  ico0  10218  ioc0  10219  expclzaplem  10500  expnegzap  10510  expaddzap  10520  expmulzap  10522  omgadd  10737  shftuz  10781  cau3lem  11078  climuni  11256  efltim  11661  divalgb  11884  ndvdssub  11889  dvdsgcd  11967  lcmgcdlem  12031  qredeu  12051  isprm3  12072  prmdvdsexpr  12104  prmexpb  12105  fermltl  12188  coprimeprodsq  12211  pythagtrip  12237  pcpremul  12247  pcdvdsb  12273  pc2dvds  12283  ctinf  12385  cnntr  13019  cncnp2m  13025  cnptoprest  13033  lmtopcnp  13044  cnmptcom  13092  hmeof1o  13103  blpnf  13194  blssps  13221  blss  13222  blssec  13232  neibl  13285  climcncf  13365  cnplimcim  13430  bj-peano4  13990  triap  14061