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  2848  moi  3000  ifnebibdc  3668  sotricim  4444  elirr  4663  en2lp  4676  suc11g  4679  3optocl  4828  sefvex  5691  f1oresrab  5842  ovmpos  6177  ov2gf  6178  poxp  6428  brtposg  6485  dfsmo2  6518  smoiun  6532  tfrlemibxssdm  6558  tfr1onlemsucfn  6571  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfr1onlemaccex  6579  tfr1onlemres  6580  tfrcllemsucfn  6584  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcllemaccex  6592  tfrcllemres  6593  tfrcl  6595  nnsucsssuc  6725  nnaordi  6741  nnawordex  6762  mapvalg  6892  pmvalg  6893  elmapg  6895  xpdom3m  7085  ordiso  7327  ctssdc  7404  pr2ne  7489  ltbtwnnqq  7730  prarloclem4  7813  addlocpr  7851  1idprl  7905  1idpru  7906  ltexprlemrnd  7920  recexprlemrnd  7944  recexprlem1ssl  7948  recexprlem1ssu  7949  recexprlemss1l  7950  recexprlemss1u  7951  aptisr  8094  axpre-apti  8200  ltxrlt  8339  axapti  8344  lttri3  8353  reapti  8853  apreap  8861  msqge0  8890  mulge0  8893  recexap  8927  mulap0b  8929  lt2msq  9160  zaddcl  9617  zdiv  9666  zextlt  9670  prime  9677  uzind2  9690  fzind  9693  lbzbi  9948  xltneg  10169  xlt2add  10213  iocssre  10286  icossre  10287  iccssre  10288  fzen  10377  rebtwn2zlemshrink  10613  qbtwnxr  10617  ioo0  10619  ioom  10620  ico0  10621  ioc0  10622  expclzaplem  10925  expnegzap  10935  expaddzap  10945  expmulzap  10947  omgadd  11166  elovmpowrd  11266  ccatopth2  11409  pfxccatin12  11425  shftuz  11502  cau3lem  11799  climuni  11978  efltim  12384  divalgb  12611  ndvdssub  12616  bitsfzo  12641  dvdsgcd  12708  lcmgcdlem  12774  qredeu  12794  isprm3  12815  prmdvdsexpr  12847  prmexpb  12848  fermltl  12931  coprimeprodsq  12955  pythagtrip  12981  pcpremul  12991  pcdvdsb  13018  pc2dvds  13028  4sqlem12  13100  4sqlem18  13106  ctinf  13181  mulgaddcom  13863  ghmrn  13974  dvdsunit  14257  unitmulclb  14259  lmodvsdi  14459  lss0cl  14517  cnntr  15090  cncnp2m  15096  cnptoprest  15104  lmtopcnp  15115  cnmptcom  15163  hmeof1o  15174  blpnf  15265  blssps  15292  blss  15293  blssec  15303  neibl  15356  climcncf  15449  cnplimcim  15532  plyadd  15616  plymul  15617  upgredg2vtx  16143  bj-peano4  16725  triap  16813