Theorem 3expia 1231

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

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

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 1006

This theorem is referenced by:  ad5ant125  1267  mp3an3  1362  3gencl  2837  moi  2989  ifnebibdc  3651  sotricim  4420  elirr  4639  en2lp  4652  suc11g  4655  3optocl  4804  sefvex  5660  f1oresrab  5812  ovmpos  6145  ov2gf  6146  poxp  6397  brtposg  6420  dfsmo2  6453  smoiun  6467  tfrlemibxssdm  6493  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  nnsucsssuc  6660  nnaordi  6676  nnawordex  6697  mapvalg  6827  pmvalg  6828  elmapg  6830  xpdom3m  7018  ordiso  7235  ctssdc  7312  pr2ne  7397  ltbtwnnqq  7635  prarloclem4  7718  addlocpr  7756  1idprl  7810  1idpru  7811  ltexprlemrnd  7825  recexprlemrnd  7849  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  aptisr  7999  axpre-apti  8105  ltxrlt  8245  axapti  8250  lttri3  8259  reapti  8759  apreap  8767  msqge0  8796  mulge0  8799  recexap  8833  mulap0b  8835  lt2msq  9066  zaddcl  9519  zdiv  9568  zextlt  9572  prime  9579  uzind2  9592  fzind  9595  lbzbi  9850  xltneg  10071  xlt2add  10115  iocssre  10188  icossre  10189  iccssre  10190  fzen  10278  rebtwn2zlemshrink  10513  qbtwnxr  10517  ioo0  10519  ioom  10520  ico0  10521  ioc0  10522  expclzaplem  10825  expnegzap  10835  expaddzap  10845  expmulzap  10847  omgadd  11065  elovmpowrd  11155  ccatopth2  11298  pfxccatin12  11314  shftuz  11378  cau3lem  11675  climuni  11854  efltim  12260  divalgb  12487  ndvdssub  12492  bitsfzo  12517  dvdsgcd  12584  lcmgcdlem  12650  qredeu  12670  isprm3  12691  prmdvdsexpr  12723  prmexpb  12724  fermltl  12807  coprimeprodsq  12831  pythagtrip  12857  pcpremul  12867  pcdvdsb  12894  pc2dvds  12904  4sqlem12  12976  4sqlem18  12982  ctinf  13052  mulgaddcom  13734  ghmrn  13845  dvdsunit  14128  unitmulclb  14130  lmodvsdi  14327  lss0cl  14385  cnntr  14951  cncnp2m  14957  cnptoprest  14965  lmtopcnp  14976  cnmptcom  15024  hmeof1o  15035  blpnf  15126  blssps  15153  blss  15154  blssec  15164  neibl  15217  climcncf  15310  cnplimcim  15393  plyadd  15477  plymul  15478  upgredg2vtx  16001  bj-peano4  16553  triap  16636