Theorem mpd3an3 1460

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  stoic2b  1779  elovmpo  7492  f1oeng  8714  wdomimag  9276  gruuni  10487  genpv  10686  pncan3  11159  mulsubaddmulsub  11369  infssuzle  12600  fzrevral3  13272  flflp1  13455  subsq2  13855  brfi1ind  14141  opfi1ind  14144  ccatws1ls  14271  swrdrlen  14300  pfxpfxid  14350  pfxcctswrd  14351  2cshwid  14455  caubnd  14998  dvdsmul1  15915  dvdsmul2  15916  hashbcval  16631  setsvalg  16795  ressval  16870  restval  17054  mrelatglb0  18194  imasmnd2  18337  efmndov  18435  qusinv  18730  ghminv  18756  gsmsymgrfixlem1  18950  gsmsymgreqlem2  18954  gexod  19106  lsmvalx  19159  ringrz  19742  imasring  19773  irredneg  19867  ocvin  20791  frlmiscvec  20966  evlrhm  21216  gsumsmonply1  21384  mat1mhm  21541  marrepfval  21617  marrepval0  21618  marepvfval  21622  marepvval0  21623  1elcpmat  21772  m2cpminv0  21818  idpm2idmp  21858  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  restin  22225  qtopval  22754  elqtop3  22762  elfm3  23009  flimval  23022  nmge0  23679  nmeq0  23680  nminv  23683  nmo0  23805  0nghm  23811  coemulhi  25320  isosctrlem2  25874  divsqrtsumlem  26034  2lgsoddprmlem4  26468  0uhgrrusgr  27848  frgruhgr0v  28529  nvge0  28936  nvnd  28951  dip0r  28980  dip0l  28981  nmoo0  29054  hi2eq  29368  wrdsplex  31114  resvval  31428  unitdivcld  31753  signspval  32431  satfv0  33220  ltflcei  35692  elghomlem1OLD  35970  rngorz  36008  rngonegmn1l  36026  rngonegmn1r  36027  igenval  36146  xrnidresex  36460  xrncnvepresex  36461  lfl0  37006  olj01  37166  olm11  37168  hl2at  37346  pmapeq0  37707  trlcl  38105  trlle  38125  tendoid  38714  tendo0plr  38733  tendoipl2  38739  erngmul  38747  erngmul-rN  38755  dvamulr  38953  dvavadd  38956  dvhmulr  39027  cdlemm10N  39059  repncan3  40287  pellfund14  40636  mendmulr  40929  fmuldfeq  43014  stoweidlem19  43450  stoweidlem26  43457  addsubeq0  44676  prelspr  44826  lincval1  45648