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  6216  rdgexgg  6275  oaexg  6344  omexg  6347  oeiexg  6349  oav2  6359  nnaordex  6423  mulidnq  7197  1idpru  7399  addgt0sr  7583  muladd11  7895  cnegex  7940  negsubdi  8018  renegcl  8023  mulneg1  8157  ltaddpos  8214  addge01  8234  rimul  8347  recclap  8439  recidap  8446  recidap2  8447  recdivap2  8485  divdiv23apzi  8525  ltmul12a  8618  lemul12a  8620  mulgt1  8621  ltmulgt11  8622  gt0div  8628  ge0div  8629  ltdiv23i  8684  8th4div3  8939  gtndiv  9146  nn0ind  9165  fnn0ind  9167  xrre2  9604  ioorebasg  9758  fzen  9823  elfz0ubfz0  9902  expubnd  10350  le2sq2  10368  bernneq  10412  expnbnd  10415  faclbnd6  10490  bccl  10513  hashfacen  10579  shftfval  10593  mulreap  10636  caucvgrelemrec  10751  binom1p  11254  efi4p  11424  sinadd  11443  cosadd  11444  cos2t  11457  cos2tsin  11458  absefib  11477  efieq1re  11478  demoivreALT  11480  odd2np1  11570  opoe  11592  omoe  11593  opeo  11594  omeo  11595  gcdadd  11673  gcdmultiple  11708  algcvgblem  11730  algcvga  11732  isprm3  11799  coprm  11822  bl2ioo  12711  ioo2blex  12713  sinperlem  12889