Theorem 3expia 1232

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

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

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 1007

This theorem is referenced by:  ad5ant125  1268  mp3an3  1363  3gencl  2838  moi  2990  ifnebibdc  3655  sotricim  4426  elirr  4645  en2lp  4658  suc11g  4661  3optocl  4810  sefvex  5669  f1oresrab  5820  ovmpos  6155  ov2gf  6156  poxp  6406  brtposg  6463  dfsmo2  6496  smoiun  6510  tfrlemibxssdm  6536  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  nnsucsssuc  6703  nnaordi  6719  nnawordex  6740  mapvalg  6870  pmvalg  6871  elmapg  6873  xpdom3m  7061  ordiso  7278  ctssdc  7355  pr2ne  7440  ltbtwnnqq  7678  prarloclem4  7761  addlocpr  7799  1idprl  7853  1idpru  7854  ltexprlemrnd  7868  recexprlemrnd  7892  recexprlem1ssl  7896  recexprlem1ssu  7897  recexprlemss1l  7898  recexprlemss1u  7899  aptisr  8042  axpre-apti  8148  ltxrlt  8287  axapti  8292  lttri3  8301  reapti  8801  apreap  8809  msqge0  8838  mulge0  8841  recexap  8875  mulap0b  8877  lt2msq  9108  zaddcl  9563  zdiv  9612  zextlt  9616  prime  9623  uzind2  9636  fzind  9639  lbzbi  9894  xltneg  10115  xlt2add  10159  iocssre  10232  icossre  10233  iccssre  10234  fzen  10323  rebtwn2zlemshrink  10559  qbtwnxr  10563  ioo0  10565  ioom  10566  ico0  10567  ioc0  10568  expclzaplem  10871  expnegzap  10881  expaddzap  10891  expmulzap  10893  omgadd  11111  elovmpowrd  11204  ccatopth2  11347  pfxccatin12  11363  shftuz  11440  cau3lem  11737  climuni  11916  efltim  12322  divalgb  12549  ndvdssub  12554  bitsfzo  12579  dvdsgcd  12646  lcmgcdlem  12712  qredeu  12732  isprm3  12753  prmdvdsexpr  12785  prmexpb  12786  fermltl  12869  coprimeprodsq  12893  pythagtrip  12919  pcpremul  12929  pcdvdsb  12956  pc2dvds  12966  4sqlem12  13038  4sqlem18  13044  ctinf  13114  mulgaddcom  13796  ghmrn  13907  dvdsunit  14190  unitmulclb  14192  lmodvsdi  14390  lss0cl  14448  cnntr  15019  cncnp2m  15025  cnptoprest  15033  lmtopcnp  15044  cnmptcom  15092  hmeof1o  15103  blpnf  15194  blssps  15221  blss  15222  blssec  15232  neibl  15285  climcncf  15378  cnplimcim  15461  plyadd  15545  plymul  15546  upgredg2vtx  16072  bj-peano4  16654  triap  16744