Theorem mp3an1 1255

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

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  mp3an12  1258  mp3an1i  1261  mp3anl1  1262  mp3an  1268  mp3an2i  1273  mp3an3an  1274  tfrlem9  5958  rdgexgg  5988  oaexg  6051  omexg  6054  oeiexg  6056  oav2  6066  nnaordex  6123  mulidnq  6579  1idpru  6781  addgt0sr  6952  muladd11  7241  cnegex  7286  negsubdi  7364  renegcl  7369  mulneg1  7499  ltaddpos  7556  addge01  7576  rimul  7685  recclap  7767  recidap  7774  recidap2  7775  recdivap2  7813  divdiv23apzi  7853  ltmul12a  7938  lemul12a  7940  mulgt1  7941  ltmulgt11  7942  gt0div  7948  ge0div  7949  ltdiv23i  8004  8th4div3  8250  gtndiv  8442  nn0ind  8461  fnn0ind  8463  xrre2  8888  ioorebasg  8998  fzen  9062  elfz0ubfz0  9136  frec2uzzd  9402  frec2uzsucd  9403  expubnd  9533  le2sq2  9551  bernneq  9593  expnbnd  9596  faclbnd6  9671  bccl  9694  shftfval  9709  mulreap  9751  caucvgrelemrec  9865  odd2np1  10272  opoe  10295  omoe  10296  opeo  10297  omeo  10298  gcdadd  10376  gcdmultiple  10409  algcvgblem  10431  ialgcvga  10433  isprm3  10500  coprm  10523