Theorem 3expia 1236

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

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

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 1011

This theorem is referenced by:  ad5ant125  1272  mp3an3  1367  3gencl  2856  moi  3009  ifnebibdc  3683  sotricim  4463  elirr  4683  en2lp  4696  suc11g  4699  3optocl  4848  sefvex  5711  f1oresrab  5864  ovmpos  6202  ov2gf  6203  poxp  6458  brtposg  6515  dfsmo2  6548  smoiun  6562  tfrlemibxssdm  6588  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemaccex  6609  tfr1onlemres  6610  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemaccex  6622  tfrcllemres  6623  tfrcl  6625  nnsucsssuc  6755  nnaordi  6771  nnawordex  6792  mapvalg  6922  pmvalg  6923  elmapg  6925  xpdom3m  7122  ordiso  7366  ctssdc  7443  pr2ne  7528  ltbtwnnqq  7772  prarloclem4  7855  addlocpr  7893  1idprl  7947  1idpru  7948  ltexprlemrnd  7962  recexprlemrnd  7986  recexprlem1ssl  7990  recexprlem1ssu  7991  recexprlemss1l  7992  recexprlemss1u  7993  aptisr  8136  axpre-apti  8242  ltxrlt  8381  axapti  8386  lttri3  8395  reapti  8897  apreap  8905  msqge0  8934  mulge0  8937  recexap  8971  mulap0b  8973  lt2msq  9206  zaddcl  9663  zdiv  9713  zextlt  9717  prime  9724  uzind2  9737  fzind  9740  lbzbi  9995  xltneg  10217  xlt2add  10261  iocssre  10334  icossre  10335  iccssre  10336  fzen  10426  rebtwn2zlemshrink  10666  qbtwnxr  10670  ioo0  10672  ioom  10673  ico0  10674  ioc0  10675  expclzaplem  10978  expnegzap  10988  expaddzap  10998  expmulzap  11000  omgadd  11220  elovmpowrd  11324  ccatopth2  11467  pfxccatin12  11483  shftuz  11560  cau3lem  11858  climuni  12037  efltim  12443  divalgb  12670  ndvdssub  12675  bitsfzo  12700  dvdsgcd  12767  lcmgcdlem  12833  qredeu  12853  isprm3  12874  prmdvdsexpr  12906  prmexpb  12907  fermltl  12990  coprimeprodsq  13014  pythagtrip  13040  pcpremul  13050  pcdvdsb  13077  pc2dvds  13087  4sqlem12  13159  4sqlem18  13165  ballotfilemirc  13253  ctinf  13299  mulgaddcom  13926  ghmrn  14037  dvdsunit  14392  unitmulclb  14394  lmodvsdi  14620  lss0cl  14678  cnntr  15249  cncnp2m  15255  cnptoprest  15263  lmtopcnp  15274  cnmptcom  15322  hmeof1o  15333  blpnf  15424  blssps  15451  blss  15452  blssec  15462  neibl  15515  climcncf  15608  cnplimcim  15691  plyadd  15775  plymul  15776  upgredg2vtx  16303  lealltlt2  16666  dichmul0or  16674  bj-peano4  16895  triap  16983