Theorem 3expia 1229

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expia	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1226	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 124	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

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 1004

This theorem is referenced by:  ad5ant125  1265  mp3an3  1360  3gencl  2835  moi  2987  ifnebibdc  3649  sotricim  4418  elirr  4637  en2lp  4650  suc11g  4653  3optocl  4802  sefvex  5656  f1oresrab  5808  ovmpos  6140  ov2gf  6141  poxp  6392  brtposg  6415  dfsmo2  6448  smoiun  6462  tfrlemibxssdm  6488  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemaccex  6522  tfrcllemres  6523  tfrcl  6525  nnsucsssuc  6655  nnaordi  6671  nnawordex  6692  mapvalg  6822  pmvalg  6823  elmapg  6825  xpdom3m  7013  ordiso  7226  ctssdc  7303  pr2ne  7388  ltbtwnnqq  7625  prarloclem4  7708  addlocpr  7746  1idprl  7800  1idpru  7801  ltexprlemrnd  7815  recexprlemrnd  7839  recexprlem1ssl  7843  recexprlem1ssu  7844  recexprlemss1l  7845  recexprlemss1u  7846  aptisr  7989  axpre-apti  8095  ltxrlt  8235  axapti  8240  lttri3  8249  reapti  8749  apreap  8757  msqge0  8786  mulge0  8789  recexap  8823  mulap0b  8825  lt2msq  9056  zaddcl  9509  zdiv  9558  zextlt  9562  prime  9569  uzind2  9582  fzind  9585  lbzbi  9840  xltneg  10061  xlt2add  10105  iocssre  10178  icossre  10179  iccssre  10180  fzen  10268  rebtwn2zlemshrink  10503  qbtwnxr  10507  ioo0  10509  ioom  10510  ico0  10511  ioc0  10512  expclzaplem  10815  expnegzap  10825  expaddzap  10835  expmulzap  10837  omgadd  11055  elovmpowrd  11145  ccatopth2  11288  pfxccatin12  11304  shftuz  11368  cau3lem  11665  climuni  11844  efltim  12249  divalgb  12476  ndvdssub  12481  bitsfzo  12506  dvdsgcd  12573  lcmgcdlem  12639  qredeu  12659  isprm3  12680  prmdvdsexpr  12712  prmexpb  12713  fermltl  12796  coprimeprodsq  12820  pythagtrip  12846  pcpremul  12856  pcdvdsb  12883  pc2dvds  12893  4sqlem12  12965  4sqlem18  12971  ctinf  13041  mulgaddcom  13723  ghmrn  13834  dvdsunit  14116  unitmulclb  14118  lmodvsdi  14315  lss0cl  14373  cnntr  14939  cncnp2m  14945  cnptoprest  14953  lmtopcnp  14964  cnmptcom  15012  hmeof1o  15023  blpnf  15114  blssps  15141  blss  15142  blssec  15152  neibl  15205  climcncf  15298  cnplimcim  15381  plyadd  15465  plymul  15466  upgredg2vtx  15987  bj-peano4  16486  triap  16569