Theorem mp3an3 1367

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

Hypotheses

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

Assertion

Ref	Expression
mp3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 ⊢ 𝜒
2		mp3an3.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expia 1236	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 15	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3an13  1369  mp3an23  1370  mp3anl3  1374  opelxp  4806  funimaexg  5468  ov  6211  ovmpoa  6222  ovmpo  6227  ovtposg  6535  oaword1  6749  th3q  6919  enrefg  7056  f1imaen  7087  mapxpen  7154  pw1fin  7223  xpfi  7245  djucomen  7578  addnnnq0  7822  mulnnnq0  7823  prarloclemcalc  7875  genpelxp  7884  genpprecll  7887  genppreclu  7888  addsrpr  8118  mulsrpr  8119  gt0srpr  8121  mulrid  8329  ltneg  8797  leneg  8800  suble0  8811  div1  9041  nnaddcl  9333  nnmulcl  9334  nnge1  9336  nnsub  9352  2halves  9545  halfaddsub  9550  addltmul  9553  zleltp1  9709  nnaddm1cl  9715  zextlt  9748  peano5uzti  9764  eluzp1p1  9963  uzaddcl  10001  znq  10039  xrre  10238  xrre2  10239  fzshftral  10531  nninfinf  10900  expn1ap0  11006  expadd  11038  expmul  11041  expubnd  11053  sqmul  11058  bernneq  11118  sqrecapd  11135  faclbnd2  11201  faclbnd6  11203  fihashssdif  11280  ccatlcan  11511  ccatrcan  11512  shftval3  11613  caucvgre  11768  leabs  11861  ltabs  11875  caubnd2  11905  efexp  12473  efival  12523  cos01gt0  12554  odd2np1  12664  halfleoddlt  12685  omoe  12687  opeo  12688  gcdmultiple  12821  sqgcd  12830  nn0seqcvgd  12843  phiprmpw  13028  eulerthlemth  13038  odzcllem  13049  pcelnn  13128  4sqlem3  13197  lsp0  14868  lss0v  14875  zndvds0  15093  ntrin  15367  txuni2  15499  txopn  15508  xblpnfps  15641  xblpnf  15642  bl2in  15646  unirnblps  15665  unirnbl  15666  blpnfctr  15682  plyconst  15988  plyid  15989  sincosq1eq  16083  rpcxpp1  16156  rplogb1  16201  ppiqub  16310  bposlem1  16328  bposlem2  16329  bposlem9  16336