Theorem mp3an1 1303

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 1183	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 421	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

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

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 965

This theorem is referenced by:  mp3an12  1306  mp3an1i  1309  mp3anl1  1310  mp3an  1316  mp3an2i  1321  mp3an3an  1322  tfrlem9  6224  rdgexgg  6283  oaexg  6352  omexg  6355  oeiexg  6357  oav2  6367  nnaordex  6431  mulidnq  7221  1idpru  7423  addgt0sr  7607  muladd11  7919  cnegex  7964  negsubdi  8042  renegcl  8047  mulneg1  8181  ltaddpos  8238  addge01  8258  rimul  8371  recclap  8463  recidap  8470  recidap2  8471  recdivap2  8509  divdiv23apzi  8549  ltmul12a  8642  lemul12a  8644  mulgt1  8645  ltmulgt11  8646  gt0div  8652  ge0div  8653  ltdiv23i  8708  8th4div3  8963  gtndiv  9170  nn0ind  9189  fnn0ind  9191  xrre2  9634  ioorebasg  9788  fzen  9854  elfz0ubfz0  9933  expubnd  10381  le2sq2  10399  bernneq  10443  expnbnd  10446  faclbnd6  10522  bccl  10545  hashfacen  10611  shftfval  10625  mulreap  10668  caucvgrelemrec  10783  binom1p  11286  efi4p  11460  sinadd  11479  cosadd  11480  cos2t  11493  cos2tsin  11494  absefib  11513  efieq1re  11514  demoivreALT  11516  odd2np1  11606  opoe  11628  omoe  11629  opeo  11630  omeo  11631  gcdadd  11709  gcdmultiple  11744  algcvgblem  11766  algcvga  11768  isprm3  11835  coprm  11858  bl2ioo  12750  ioo2blex  12752  sinperlem  12937  logge0  13009