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  1337  3gencl  2786  moi  2935  ifnebibdc  3592  sotricim  4344  elirr  4561  en2lp  4574  suc11g  4577  3optocl  4725  sefvex  5558  f1oresrab  5705  ovmpos  6024  ov2gf  6025  poxp  6261  brtposg  6283  dfsmo2  6316  smoiun  6330  tfrlemibxssdm  6356  tfr1onlemsucfn  6369  tfr1onlemsucaccv  6370  tfr1onlembxssdm  6372  tfr1onlembfn  6373  tfr1onlemaccex  6377  tfr1onlemres  6378  tfrcllemsucfn  6382  tfrcllemsucaccv  6383  tfrcllembxssdm  6385  tfrcllembfn  6386  tfrcllemaccex  6390  tfrcllemres  6391  tfrcl  6393  nnsucsssuc  6521  nnaordi  6537  nnawordex  6558  mapvalg  6688  pmvalg  6689  elmapg  6691  xpdom3m  6864  ordiso  7069  ctssdc  7146  pr2ne  7226  ltbtwnnqq  7449  prarloclem4  7532  addlocpr  7570  1idprl  7624  1idpru  7625  ltexprlemrnd  7639  recexprlemrnd  7663  recexprlem1ssl  7667  recexprlem1ssu  7668  recexprlemss1l  7669  recexprlemss1u  7670  aptisr  7813  axpre-apti  7919  ltxrlt  8058  axapti  8063  lttri3  8072  reapti  8571  apreap  8579  msqge0  8608  mulge0  8611  recexap  8645  mulap0b  8647  lt2msq  8878  zaddcl  9328  zdiv  9376  zextlt  9380  prime  9387  uzind2  9400  fzind  9403  lbzbi  9652  xltneg  9872  xlt2add  9916  iocssre  9989  icossre  9990  iccssre  9991  fzen  10079  rebtwn2zlemshrink  10290  qbtwnxr  10294  ioo0  10296  ioom  10297  ico0  10298  ioc0  10299  expclzaplem  10584  expnegzap  10594  expaddzap  10604  expmulzap  10606  omgadd  10823  shftuz  10867  cau3lem  11164  climuni  11342  efltim  11747  divalgb  11971  ndvdssub  11976  dvdsgcd  12054  lcmgcdlem  12120  qredeu  12140  isprm3  12161  prmdvdsexpr  12193  prmexpb  12194  fermltl  12277  coprimeprodsq  12300  pythagtrip  12326  pcpremul  12336  pcdvdsb  12363  pc2dvds  12373  4sqlem12  12445  4sqlem18  12451  ctinf  12492  mulgaddcom  13111  ghmrn  13221  dvdsunit  13487  unitmulclb  13489  lmodvsdi  13652  lss0cl  13710  cnntr  14210  cncnp2m  14216  cnptoprest  14224  lmtopcnp  14235  cnmptcom  14283  hmeof1o  14294  blpnf  14385  blssps  14412  blss  14413  blssec  14423  neibl  14476  climcncf  14556  cnplimcim  14621  bj-peano4  15193  triap  15265