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 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ad5ant125  1272  mp3an3  1367  3gencl  2856  moi  3009  ifnebibdc  3686  sotricim  4468  elirr  4688  en2lp  4701  suc11g  4704  3optocl  4853  sefvex  5716  f1oresrab  5873  ovmpos  6212  ov2gf  6213  poxp  6468  brtposg  6525  dfsmo2  6558  smoiun  6572  tfrlemibxssdm  6598  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  nnsucsssuc  6765  nnaordi  6781  nnawordex  6802  mapvalg  6932  pmvalg  6933  elmapg  6935  xpdom3m  7132  ordiso  7377  ctssdc  7454  pr2ne  7539  ltbtwnnqq  7783  prarloclem4  7866  addlocpr  7904  1idprl  7958  1idpru  7959  ltexprlemrnd  7973  recexprlemrnd  7997  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  recexprlemss1u  8004  aptisr  8147  axpre-apti  8253  ltxrlt  8392  axapti  8397  lttri3  8406  reapti  8910  apreap  8918  msqge0  8947  mulge0  8950  recexap  8984  mulap0b  8986  lt2msq  9219  zaddcl  9689  zdiv  9739  zextlt  9743  prime  9750  uzind2  9763  fzind  9766  lbzbi  10026  xltneg  10249  xlt2add  10293  iocssre  10366  icossre  10367  iccssre  10368  fzen  10458  rebtwn2zlemshrink  10699  qbtwnxr  10703  ioo0  10705  ioom  10706  ico0  10707  ioc0  10708  expclzaplem  11015  expnegzap  11025  expaddzap  11035  expmulzap  11037  omgadd  11258  elovmpowrd  11362  ccatopth2  11505  pfxccatin12  11521  shftuz  11598  cau3lem  11897  climuni  12078  efltim  12484  divalgb  12711  ndvdssub  12716  bitsfzo  12741  dvdsgcd  12808  lcmgcdlem  12874  qredeu  12894  isprm3  12915  prmdvdsexpr  12948  prmexpb  12949  fermltl  13035  coprimeprodsq  13059  pythagtrip  13085  pcpremul  13095  pcdvdsb  13122  pc2dvds  13132  4sqlem12  13204  4sqlem18  13210  ballotfilemirc  13327  ctinf  13373  mulgaddcom  14002  ghmrn  14113  dvdsunit  14503  unitmulclb  14505  lmodvsdi  14732  lss0cl  14790  cnntr  15417  cncnp2m  15423  cnptoprest  15431  lmtopcnp  15442  cnmptcom  15490  hmeof1o  15501  blpnf  15592  blssps  15619  blss  15620  blssec  15630  neibl  15683  climcncf  15776  cnplimcim  15859  plyadd  15943  plymul  15944  chtublem  16256  bposlem3  16274  upgredg2vtx  16555  lealltlt2  16918  dichmul0or  16926  bj-peano4  17147  triap  17244