Theorem 3expia 1207

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

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

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 982

This theorem is referenced by:  ad5ant125  1243  mp3an3  1338  3gencl  2805  moi  2955  ifnebibdc  3614  sotricim  4368  elirr  4587  en2lp  4600  suc11g  4603  3optocl  4751  sefvex  5591  f1oresrab  5739  ovmpos  6059  ov2gf  6060  poxp  6308  brtposg  6330  dfsmo2  6363  smoiun  6377  tfrlemibxssdm  6403  tfr1onlemsucfn  6416  tfr1onlemsucaccv  6417  tfr1onlembxssdm  6419  tfr1onlembfn  6420  tfr1onlemaccex  6424  tfr1onlemres  6425  tfrcllemsucfn  6429  tfrcllemsucaccv  6430  tfrcllembxssdm  6432  tfrcllembfn  6433  tfrcllemaccex  6437  tfrcllemres  6438  tfrcl  6440  nnsucsssuc  6568  nnaordi  6584  nnawordex  6605  mapvalg  6735  pmvalg  6736  elmapg  6738  xpdom3m  6911  ordiso  7120  ctssdc  7197  pr2ne  7282  ltbtwnnqq  7510  prarloclem4  7593  addlocpr  7631  1idprl  7685  1idpru  7686  ltexprlemrnd  7700  recexprlemrnd  7724  recexprlem1ssl  7728  recexprlem1ssu  7729  recexprlemss1l  7730  recexprlemss1u  7731  aptisr  7874  axpre-apti  7980  ltxrlt  8120  axapti  8125  lttri3  8134  reapti  8634  apreap  8642  msqge0  8671  mulge0  8674  recexap  8708  mulap0b  8710  lt2msq  8941  zaddcl  9394  zdiv  9443  zextlt  9447  prime  9454  uzind2  9467  fzind  9470  lbzbi  9719  xltneg  9940  xlt2add  9984  iocssre  10057  icossre  10058  iccssre  10059  fzen  10147  rebtwn2zlemshrink  10377  qbtwnxr  10381  ioo0  10383  ioom  10384  ico0  10385  ioc0  10386  expclzaplem  10689  expnegzap  10699  expaddzap  10709  expmulzap  10711  omgadd  10928  elovmpowrd  11010  shftuz  11047  cau3lem  11344  climuni  11523  efltim  11928  divalgb  12155  ndvdssub  12160  bitsfzo  12185  dvdsgcd  12252  lcmgcdlem  12318  qredeu  12338  isprm3  12359  prmdvdsexpr  12391  prmexpb  12392  fermltl  12475  coprimeprodsq  12499  pythagtrip  12525  pcpremul  12535  pcdvdsb  12562  pc2dvds  12572  4sqlem12  12644  4sqlem18  12650  ctinf  12720  mulgaddcom  13400  ghmrn  13511  dvdsunit  13792  unitmulclb  13794  lmodvsdi  13991  lss0cl  14049  cnntr  14615  cncnp2m  14621  cnptoprest  14629  lmtopcnp  14640  cnmptcom  14688  hmeof1o  14699  blpnf  14790  blssps  14817  blss  14818  blssec  14828  neibl  14881  climcncf  14974  cnplimcim  15057  plyadd  15141  plymul  15142  bj-peano4  15755  triap  15832