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  7376  ctssdc  7453  pr2ne  7538  ltbtwnnqq  7782  prarloclem4  7865  addlocpr  7903  1idprl  7957  1idpru  7958  ltexprlemrnd  7972  recexprlemrnd  7996  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  aptisr  8146  axpre-apti  8252  ltxrlt  8391  axapti  8396  lttri3  8405  reapti  8909  apreap  8917  msqge0  8946  mulge0  8949  recexap  8983  mulap0b  8985  lt2msq  9218  zaddcl  9688  zdiv  9738  zextlt  9742  prime  9749  uzind2  9762  fzind  9765  lbzbi  10025  xltneg  10248  xlt2add  10292  iocssre  10365  icossre  10366  iccssre  10367  fzen  10457  rebtwn2zlemshrink  10698  qbtwnxr  10702  ioo0  10704  ioom  10705  ico0  10706  ioc0  10707  expclzaplem  11013  expnegzap  11023  expaddzap  11033  expmulzap  11035  omgadd  11256  elovmpowrd  11360  ccatopth2  11503  pfxccatin12  11519  shftuz  11596  cau3lem  11895  climuni  12075  efltim  12481  divalgb  12708  ndvdssub  12713  bitsfzo  12738  dvdsgcd  12805  lcmgcdlem  12871  qredeu  12891  isprm3  12912  prmdvdsexpr  12945  prmexpb  12946  fermltl  13032  coprimeprodsq  13056  pythagtrip  13082  pcpremul  13092  pcdvdsb  13119  pc2dvds  13129  4sqlem12  13201  4sqlem18  13207  ballotfilemirc  13324  ctinf  13370  mulgaddcom  13998  ghmrn  14109  dvdsunit  14468  unitmulclb  14470  lmodvsdi  14697  lss0cl  14755  cnntr  15375  cncnp2m  15381  cnptoprest  15389  lmtopcnp  15400  cnmptcom  15448  hmeof1o  15459  blpnf  15550  blssps  15577  blss  15578  blssec  15588  neibl  15641  climcncf  15734  cnplimcim  15817  plyadd  15901  plymul  15902  bposlem3  16211  upgredg2vtx  16487  lealltlt2  16850  dichmul0or  16858  bj-peano4  17079  triap  17176