Theorem mp3an1 1302

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

Hypotheses

Ref	Expression
mp3an1.1	⊢ 𝜑
mp3an1.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an1	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 ⊢ 𝜑
2		mp3an1.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expb 1182	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 420	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  mp3an12  1305  mp3an1i  1308  mp3anl1  1309  mp3an  1315  mp3an2i  1320  mp3an3an  1321  tfrlem9  6209  rdgexgg  6268  oaexg  6337  omexg  6340  oeiexg  6342  oav2  6352  nnaordex  6416  mulidnq  7190  1idpru  7392  addgt0sr  7576  muladd11  7888  cnegex  7933  negsubdi  8011  renegcl  8016  mulneg1  8150  ltaddpos  8207  addge01  8227  rimul  8340  recclap  8432  recidap  8439  recidap2  8440  recdivap2  8478  divdiv23apzi  8518  ltmul12a  8611  lemul12a  8613  mulgt1  8614  ltmulgt11  8615  gt0div  8621  ge0div  8622  ltdiv23i  8677  8th4div3  8932  gtndiv  9139  nn0ind  9158  fnn0ind  9160  xrre2  9597  ioorebasg  9751  fzen  9816  elfz0ubfz0  9895  expubnd  10343  le2sq2  10361  bernneq  10405  expnbnd  10408  faclbnd6  10483  bccl  10506  hashfacen  10572  shftfval  10586  mulreap  10629  caucvgrelemrec  10744  binom1p  11247  efi4p  11413  sinadd  11432  cosadd  11433  cos2t  11446  cos2tsin  11447  absefib  11466  efieq1re  11467  demoivreALT  11469  odd2np1  11559  opoe  11581  omoe  11582  opeo  11583  omeo  11584  gcdadd  11662  gcdmultiple  11697  algcvgblem  11719  algcvga  11721  isprm3  11788  coprm  11811  bl2ioo  12700  ioo2blex  12702  sinperlem  12878