Theorem mp3an12i 1378

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  funopsn  5865  map1  7067  exmidpw2en  7185  2omapen  7283  suplocsrlempr  8138  geo2lim  12227  fprodge0  12348  fprodge1  12350  3dvds  12575  oddp1d2  12601  bezoutlema  12720  bezoutlemb  12721  pythagtriplem1  12988  exmidunben  13261  psrelbas  14956  psraddcl  14961  psr0cl  14962  psr0lid  14963  psrnegcl  14964  psrlinv  14965  psrgrp  14966  psr1clfi  14969  mplsubgfilemcl  14980  ismet  15335  isxmet  15336  dvidrelem  15683  coseq0negpitopi  15827  cosq34lt1  15841  cos02pilt1  15842  logdivlti  15872  1sgm2ppw  15989  lgseisenlem1  16069  lgseisen  16073  lgsquad3  16083  m1lgs  16084  pw1mapen  16896