Theorem mpd3an3 1458

Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)

Hypotheses

Ref	Expression
mpd3an3.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
mpd3an3.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mpd3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mpd3an3

Step	Hyp	Ref	Expression
1		mpd3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		mpd3an3.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expa 1114	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpdan 685	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  stoic2b  1776  elovmpo  7390  f1oeng  8528  wdomimag  9051  gruuni  10222  genpv  10421  pncan3  10894  mulsubaddmulsub  11104  infssuzle  12332  fzrevral3  12995  flflp1  13178  subsq2  13574  brfi1ind  13858  opfi1ind  13861  ccatws1ls  13992  swrdrlen  14021  pfxpfxid  14071  pfxcctswrd  14072  2cshwid  14176  caubnd  14718  dvdsmul1  15631  dvdsmul2  15632  hashbcval  16338  setsvalg  16512  ressval  16551  restval  16700  mrelatglb0  17795  imasmnd2  17948  efmndov  18046  qusinv  18339  ghminv  18365  gsmsymgrfixlem1  18555  gsmsymgreqlem2  18559  gexod  18711  lsmvalx  18764  ringrz  19338  imasring  19369  irredneg  19460  evlrhm  20309  gsumsmonply1  20471  ocvin  20818  frlmiscvec  20993  mat1mhm  21093  marrepfval  21169  marrepval0  21170  marepvfval  21174  marepvval0  21175  1elcpmat  21323  m2cpminv0  21369  idpm2idmp  21409  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  restin  21774  qtopval  22303  elqtop3  22311  elfm3  22558  flimval  22571  nmge0  23226  nmeq0  23227  nminv  23230  nmo0  23344  0nghm  23350  coemulhi  24844  isosctrlem2  25397  divsqrtsumlem  25557  2lgsoddprmlem4  25991  0uhgrrusgr  27360  frgruhgr0v  28043  nvge0  28450  nvnd  28465  dip0r  28494  dip0l  28495  nmoo0  28568  hi2eq  28882  wrdsplex  30614  resvval  30900  unitdivcld  31144  signspval  31822  satfv0  32605  ltflcei  34895  elghomlem1OLD  35178  rngorz  35216  rngonegmn1l  35234  rngonegmn1r  35235  igenval  35354  xrnidresex  35670  xrncnvepresex  35671  lfl0  36216  olj01  36376  olm11  36378  hl2at  36556  pmapeq0  36917  trlcl  37315  trlle  37335  tendoid  37924  tendo0plr  37943  tendoipl2  37949  erngmul  37957  erngmul-rN  37965  dvamulr  38163  dvavadd  38166  dvhmulr  38237  cdlemm10N  38269  repncan3  39233  pellfund14  39515  mendmulr  39808  fmuldfeq  41884  stoweidlem19  42324  stoweidlem26  42331  addsubeq0  43516  prelspr  43668  lincval1  44494