Theorem mp3an12i 1354

Description: mp3an 1350 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses

Ref	Expression
mp3an12i.1	⊢ 𝜑
mp3an12i.2	⊢ 𝜓
mp3an12i.3	⊢ (𝜒 → 𝜃)
mp3an12i.4	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
mp3an12i	⊢ (𝜒 → 𝜏)

Proof of Theorem mp3an12i

Step	Hyp	Ref	Expression
1		mp3an12i.3	. 2 ⊢ (𝜒 → 𝜃)
2		mp3an12i.1	. . 3 ⊢ 𝜑
3		mp3an12i.2	. . 3 ⊢ 𝜓
4		mp3an12i.4	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	mp3an12 1340	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 14	1 ⊢ (𝜒 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  funopsn  5764  map1  6906  exmidpw2en  7011  suplocsrlempr  7922  geo2lim  11860  fprodge0  11981  fprodge1  11983  3dvds  12208  oddp1d2  12234  bezoutlema  12353  bezoutlemb  12354  pythagtriplem1  12621  exmidunben  12830  psrelbas  14470  psraddcl  14475  psr0cl  14476  psr0lid  14477  psrnegcl  14478  psrlinv  14479  psrgrp  14480  psr1clfi  14483  mplsubgfilemcl  14494  ismet  14849  isxmet  14850  dvidrelem  15197  coseq0negpitopi  15341  cosq34lt1  15355  cos02pilt1  15356  logdivlti  15386  1sgm2ppw  15500  lgseisenlem1  15580  lgseisen  15584  lgsquad3  15594  m1lgs  15595  2omapen  15970