Theorem 3expia 1208

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 1205	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 124	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

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

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 983

This theorem is referenced by:  ad5ant125  1244  mp3an3  1339  3gencl  2808  moi  2960  ifnebibdc  3620  sotricim  4378  elirr  4597  en2lp  4610  suc11g  4613  3optocl  4761  sefvex  5610  f1oresrab  5758  ovmpos  6082  ov2gf  6083  poxp  6331  brtposg  6353  dfsmo2  6386  smoiun  6400  tfrlemibxssdm  6426  tfr1onlemsucfn  6439  tfr1onlemsucaccv  6440  tfr1onlembxssdm  6442  tfr1onlembfn  6443  tfr1onlemaccex  6447  tfr1onlemres  6448  tfrcllemsucfn  6452  tfrcllemsucaccv  6453  tfrcllembxssdm  6455  tfrcllembfn  6456  tfrcllemaccex  6460  tfrcllemres  6461  tfrcl  6463  nnsucsssuc  6591  nnaordi  6607  nnawordex  6628  mapvalg  6758  pmvalg  6759  elmapg  6761  xpdom3m  6944  ordiso  7153  ctssdc  7230  pr2ne  7315  ltbtwnnqq  7548  prarloclem4  7631  addlocpr  7669  1idprl  7723  1idpru  7724  ltexprlemrnd  7738  recexprlemrnd  7762  recexprlem1ssl  7766  recexprlem1ssu  7767  recexprlemss1l  7768  recexprlemss1u  7769  aptisr  7912  axpre-apti  8018  ltxrlt  8158  axapti  8163  lttri3  8172  reapti  8672  apreap  8680  msqge0  8709  mulge0  8712  recexap  8746  mulap0b  8748  lt2msq  8979  zaddcl  9432  zdiv  9481  zextlt  9485  prime  9492  uzind2  9505  fzind  9508  lbzbi  9757  xltneg  9978  xlt2add  10022  iocssre  10095  icossre  10096  iccssre  10097  fzen  10185  rebtwn2zlemshrink  10418  qbtwnxr  10422  ioo0  10424  ioom  10425  ico0  10426  ioc0  10427  expclzaplem  10730  expnegzap  10740  expaddzap  10750  expmulzap  10752  omgadd  10969  elovmpowrd  11057  ccatopth2  11193  shftuz  11203  cau3lem  11500  climuni  11679  efltim  12084  divalgb  12311  ndvdssub  12316  bitsfzo  12341  dvdsgcd  12408  lcmgcdlem  12474  qredeu  12494  isprm3  12515  prmdvdsexpr  12547  prmexpb  12548  fermltl  12631  coprimeprodsq  12655  pythagtrip  12681  pcpremul  12691  pcdvdsb  12718  pc2dvds  12728  4sqlem12  12800  4sqlem18  12806  ctinf  12876  mulgaddcom  13557  ghmrn  13668  dvdsunit  13949  unitmulclb  13951  lmodvsdi  14148  lss0cl  14206  cnntr  14772  cncnp2m  14778  cnptoprest  14786  lmtopcnp  14797  cnmptcom  14845  hmeof1o  14856  blpnf  14947  blssps  14974  blss  14975  blssec  14985  neibl  15038  climcncf  15131  cnplimcim  15214  plyadd  15298  plymul  15299  bj-peano4  16029  triap  16109