Theorem 3expia 1231

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

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

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 1006

This theorem is referenced by:  ad5ant125  1267  mp3an3  1362  3gencl  2837  moi  2989  ifnebibdc  3651  sotricim  4420  elirr  4639  en2lp  4652  suc11g  4655  3optocl  4804  sefvex  5660  f1oresrab  5812  ovmpos  6145  ov2gf  6146  poxp  6397  brtposg  6420  dfsmo2  6453  smoiun  6467  tfrlemibxssdm  6493  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  nnsucsssuc  6660  nnaordi  6676  nnawordex  6697  mapvalg  6827  pmvalg  6828  elmapg  6830  xpdom3m  7018  ordiso  7235  ctssdc  7312  pr2ne  7397  ltbtwnnqq  7635  prarloclem4  7718  addlocpr  7756  1idprl  7810  1idpru  7811  ltexprlemrnd  7825  recexprlemrnd  7849  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  aptisr  7999  axpre-apti  8105  ltxrlt  8245  axapti  8250  lttri3  8259  reapti  8759  apreap  8767  msqge0  8796  mulge0  8799  recexap  8833  mulap0b  8835  lt2msq  9066  zaddcl  9519  zdiv  9568  zextlt  9572  prime  9579  uzind2  9592  fzind  9595  lbzbi  9850  xltneg  10071  xlt2add  10115  iocssre  10188  icossre  10189  iccssre  10190  fzen  10278  rebtwn2zlemshrink  10514  qbtwnxr  10518  ioo0  10520  ioom  10521  ico0  10522  ioc0  10523  expclzaplem  10826  expnegzap  10836  expaddzap  10846  expmulzap  10848  omgadd  11066  elovmpowrd  11159  ccatopth2  11302  pfxccatin12  11318  shftuz  11382  cau3lem  11679  climuni  11858  efltim  12264  divalgb  12491  ndvdssub  12496  bitsfzo  12521  dvdsgcd  12588  lcmgcdlem  12654  qredeu  12674  isprm3  12695  prmdvdsexpr  12727  prmexpb  12728  fermltl  12811  coprimeprodsq  12835  pythagtrip  12861  pcpremul  12871  pcdvdsb  12898  pc2dvds  12908  4sqlem12  12980  4sqlem18  12986  ctinf  13056  mulgaddcom  13738  ghmrn  13849  dvdsunit  14132  unitmulclb  14134  lmodvsdi  14331  lss0cl  14389  cnntr  14955  cncnp2m  14961  cnptoprest  14969  lmtopcnp  14980  cnmptcom  15028  hmeof1o  15039  blpnf  15130  blssps  15157  blss  15158  blssec  15168  neibl  15221  climcncf  15314  cnplimcim  15397  plyadd  15481  plymul  15482  upgredg2vtx  16005  bj-peano4  16576  triap  16659