Theorem mpd3an3 1535

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 1108	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpdan 677	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  stoic2b  1819  elovmpt2  7156  f1oeng  8260  wdomimag  8781  cdaval  9327  gruuni  9957  genpv  10156  pncan3  10630  mulsubaddmulsub  10839  infssuzle  12078  fzrevral3  12745  flflp1  12927  subsq2  13292  brfi1ind  13595  opfi1ind  13598  ccatws1ls  13723  swrdrlen  13754  swrd0swrdidOLD  13821  pfxpfxid  13822  pfxcctswrd  13823  2cshwid  13965  caubnd  14505  dvdsmul1  15410  dvdsmul2  15411  hashbcval  16110  setsvalg  16284  ressval  16323  restval  16473  mrelatglb0  17571  imasmnd2  17713  qusinv  18037  ghminv  18051  symgov  18193  gexod  18385  lsmvalx  18438  ringrz  18975  imasring  19006  irredneg  19097  evlrhm  19921  gsumsmonply1  20069  ocvin  20417  frlmiscvec  20592  mat1mhm  20695  marrepfval  20771  marrepval0  20772  marepvfval  20776  marepvval0  20777  1elcpmat  20927  m2cpminv0  20973  idpm2idmp  21013  chfacfscmulgsum  21072  chfacfpmmulgsum  21076  restin  21378  qtopval  21907  elqtop3  21915  elfm3  22162  flimval  22175  nmge0  22829  nmeq0  22830  nminv  22833  nmo0  22947  0nghm  22953  coemulhi  24447  isosctrlem2  24997  divsqrtsumlem  25158  2lgsoddprmlem4  25592  0uhgrrusgr  26926  frgruhgr0v  27671  nvge0  28100  nvnd  28115  dip0r  28144  dip0l  28145  nmoo0  28218  hi2eq  28534  resvval  30389  unitdivcld  30545  wrdsplex  31217  signspval  31229  ltflcei  34022  elghomlem1OLD  34308  rngorz  34346  rngonegmn1l  34364  rngonegmn1r  34365  igenval  34484  xrnidresex  34793  xrncnvepresex  34794  lfl0  35219  olj01  35379  olm11  35381  hl2at  35559  pmapeq0  35920  trlcl  36318  trlle  36338  tendoid  36927  tendo0plr  36946  tendoipl2  36952  erngmul  36960  erngmul-rN  36968  dvamulr  37166  dvavadd  37169  dvhmulr  37240  cdlemm10N  37272  repncan3  38192  pellfund14  38422  mendmulr  38717  fmuldfeq  40723  stoweidlem19  41163  stoweidlem26  41170  addsubeq0  42338  prelspr  42425  lincval1  43223