Theorem mpd3an3 1465

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

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  stoic2b  1777  elovmpo  7613  f1oeng  8919  php  9143  nnsdomg  9211  wdomimag  9504  gruuni  10723  genpv  10922  pncan3  11400  mulsubaddmulsub  11613  infssuzle  12856  fzrevral3  13542  flflp1  13739  subsq2  14146  brfi1ind  14444  opfi1ind  14447  ccatws1ls  14569  swrdrlen  14595  pfxpfxid  14644  pfxcctswrd  14645  2cshwid  14749  caubnd  15294  dvdsmul1  16216  dvdsmul2  16217  hashbcval  16942  setsvalg  17105  ressval  17172  restval  17358  mrelatglb0  18496  imasmnd2  18711  efmndov  18818  qusinv  19131  ghminv  19164  gsmsymgrfixlem1  19368  gsmsymgreqlem2  19372  gexod  19527  lsmvalx  19580  rngrz  20113  imasring  20278  irredneg  20378  01eq0ring  20475  ocvin  21641  frlmiscvec  21816  evlrhm  22068  gsumsmonply1  22263  mat1mhm  22440  marrepfval  22516  marrepval0  22517  marepvfval  22521  marepvval0  22522  1elcpmat  22671  m2cpminv0  22717  idpm2idmp  22757  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  restin  23122  qtopval  23651  elqtop3  23659  elfm3  23906  flimval  23919  nmge0  24573  nmeq0  24574  nminv  24577  nmo0  24691  0nghm  24697  coemulhi  26227  isosctrlem2  26797  divsqrtsumlem  26958  2lgsoddprmlem4  27394  0uhgrrusgr  29664  frgruhgr0v  30351  nvge0  30760  nvnd  30775  dip0r  30804  dip0l  30805  nmoo0  30878  hi2eq  31192  wrdsplex  33028  resvval  33421  unitdivcld  34078  signspval  34729  satfv0  35571  ltflcei  37853  elghomlem1OLD  38130  rngorz  38168  rngonegmn1l  38186  rngonegmn1r  38187  igenval  38306  xrnidresex  38675  xrncnvepresex  38676  lfl0  39435  olj01  39595  olm11  39597  hl2at  39775  pmapeq0  40136  trlcl  40534  trlle  40554  tendoid  41143  tendo0plr  41162  tendoipl2  41168  erngmul  41176  erngmul-rN  41184  dvamulr  41382  dvavadd  41385  dvhmulr  41456  cdlemm10N  41488  repncan3  42747  pellfund14  43249  mendmulr  43535  onnoxpg  43779  fmuldfeq  45937  stoweidlem19  46371  stoweidlem26  46378  addsubeq0  47650  zp1modne  47700  modm1nep1  47719  prelspr  47840  lincval1  48773