Theorem 3expia 1183

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

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

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 964

This theorem is referenced by:  mp3an3  1304  3gencl  2720  moi  2867  sotricim  4245  elirr  4456  en2lp  4469  suc11g  4472  3optocl  4617  sefvex  5442  f1oresrab  5585  ovmpos  5894  ov2gf  5895  poxp  6129  brtposg  6151  dfsmo2  6184  smoiun  6198  tfrlemibxssdm  6224  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemaccex  6258  tfrcllemres  6259  tfrcl  6261  nnsucsssuc  6388  nnaordi  6404  nnawordex  6424  mapvalg  6552  pmvalg  6553  elmapg  6555  xpdom3m  6728  ordiso  6921  ctssdc  6998  pr2ne  7048  ltbtwnnqq  7223  prarloclem4  7306  addlocpr  7344  1idprl  7398  1idpru  7399  ltexprlemrnd  7413  recexprlemrnd  7437  recexprlem1ssl  7441  recexprlem1ssu  7442  recexprlemss1l  7443  recexprlemss1u  7444  aptisr  7587  axpre-apti  7693  ltxrlt  7830  axapti  7835  lttri3  7844  reapti  8341  apreap  8349  msqge0  8378  mulge0  8381  recexap  8414  mulap0b  8416  lt2msq  8644  zaddcl  9094  zdiv  9139  zextlt  9143  prime  9150  uzind2  9163  fzind  9166  lbzbi  9408  xltneg  9619  xlt2add  9663  iocssre  9736  icossre  9737  iccssre  9738  fzen  9823  rebtwn2zlemshrink  10031  qbtwnxr  10035  ioo0  10037  ioom  10038  ico0  10039  ioc0  10040  expclzaplem  10317  expnegzap  10327  expaddzap  10337  expmulzap  10339  omgadd  10548  shftuz  10589  cau3lem  10886  climuni  11062  efltim  11404  divalgb  11622  ndvdssub  11627  dvdsgcd  11700  lcmgcdlem  11758  qredeu  11778  isprm3  11799  prmdvdsexpr  11828  prmexpb  11829  ctinf  11943  cnntr  12394  cncnp2m  12400  cnptoprest  12408  lmtopcnp  12419  cnmptcom  12467  hmeof1o  12478  blpnf  12569  blssps  12596  blss  12597  blssec  12607  neibl  12660  climcncf  12740  cnplimcim  12805  bj-peano4  13153  triap  13224