Theorem mp3an12i 1382

Description: mp3an 1378 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 1368	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 14	1 ⊢ (𝜒 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  funopsn  5882  map1  7091  exmidpw2en  7209  2omapen  7309  suplocsrlempr  8164  hashf1lem1  11263  geo2lim  12261  fprodge0  12382  fprodge1  12384  3dvds  12609  oddp1d2  12635  bezoutlema  12754  bezoutlemb  12755  pythagtriplem1  13022  exmidunben  13295  psrelbas  14989  psraddcl  14994  psr0cl  14995  psr0lid  14996  psrnegcl  14997  psrlinv  14998  psrgrp  14999  psr1clfi  15002  mplsubgfilemcl  15013  ismet  15368  isxmet  15369  dvidrelem  15716  coseq0negpitopi  15860  cosq34lt1  15874  cos02pilt1  15875  logdivlti  15905  1sgm2ppw  16023  lgseisenlem1  16103  lgseisen  16107  lgsquad3  16117  m1lgs  16118  pw1mapen  16940