Theorem mpd3an3 1491

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  stoic2b  1808  elovmpo  7658  f1oeng  8981  php  9206  nnsdomg  9275  wdomimag  9565  gruuni  10866  genpv  11065  pncan3  11546  mulsubaddmulsub  11761  infssuzle  13039  fzrevral3  13728  flflp1  13927  subsq2  14335  brfi1ind  14634  opfi1ind  14637  ccatws1ls  14761  swrdrlen  14789  pfxpfxid  14838  pfxcctswrd  14839  2cshwid  14945  caubnd  15506  dvdsmul1  16427  dvdsmul2  16428  hashbcval  17160  setsvalg  17324  ressval  17391  restval  17577  mrelatglb0  18715  imasmgm2  18843  imasmnd2  18948  efmndov  19057  qusinv  19385  ghminv  19417  gsmsymgrfixlem1  19621  gsmsymgreqlem2  19625  gexod  19780  lsmvalx  19833  rngrz  20368  imasring  20540  irredneg  20640  01eq0ring  20761  ocvin  21960  frlmiscvec  22135  evlrhm  22390  gsumsmonply1  22605  mat1mhm  22779  marrepfval  22855  marrepval0  22856  marepvfval  22860  marepvval0  22861  1elcpmat  23013  m2cpminv0  23059  idpm2idmp  23099  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  restin  23464  qtopval  23994  elqtop3  24002  elfm3  24249  flimval  24262  nmge0  24916  nmeq0  24917  nminv  24920  nmo0  25034  0nghm  25040  coemulhi  26553  isosctrlem2  27129  divsqrtsumlem  27289  2lgsoddprmlem4  27724  0uhgrrusgr  30141  frgruhgr0v  30847  nvge0  31257  nvnd  31272  dip0r  31301  dip0l  31302  nmoo0  31375  hi2eq  31689  wrdsplex  33485  resvval  33872  unitdivcld  34515  signspval  35164  satfv0  36092  ltflcei  38499  elghomlem1OLD  38787  rngorz  38825  rngonegmn1l  38843  rngonegmn1r  38844  igenval  38963  xrnidresex  39330  xrncnvepresex  39331  lfl0  40090  olj01  40250  olm11  40252  hl2at  40430  pmapeq0  40791  trlcl  41189  trlle  41209  tendoid  41798  tendo0plr  41817  tendoipl2  41823  erngmul  41831  erngmul-rN  41839  dvamulr  42037  dvavadd  42040  dvhmulr  42111  cdlemm10N  42143  repncan3  43402  pellfund14  43858  mendmulr  44144  onnoxpg  44388  fmuldfeq  46539  stoweidlem19  46973  stoweidlem26  46980  addsubeq0  48310  zp1modne  48366  modm1nep1  48385  prelspr  48512  lincval1  49475