Theorem mpisyl 22

Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011.)

Hypotheses

Ref	Expression
mpisyl.1	⊢ (𝜑 → 𝜓)
mpisyl.2	⊢ 𝜒
mpisyl.3	⊢ (𝜓 → (𝜒 → 𝜃))

Assertion

Ref	Expression
mpisyl	⊢ (𝜑 → 𝜃)

Proof of Theorem mpisyl

Step	Hyp	Ref	Expression
1		mpisyl.1	. 2 ⊢ (𝜑 → 𝜓)
2		mpisyl.2	. . 3 ⊢ 𝜒
3		mpisyl.3	. . 3 ⊢ (𝜓 → (𝜒 → 𝜃))
4	2, 3	mpi 21	. 2 ⊢ (𝜓 → 𝜃)
5	1, 4	syl 18	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  moeq3  3678  fvsng  7185  fveqf1o  7311  fliftcnv  7320  fliftfun  7321  frxp3  8156  orderseqlem  8162  cnvct  9041  pwdom  9127  php  9201  ordiso  9488  ordtypelem8  9497  wdompwdom  9550  unxpwdom  9561  harwdom  9563  inf0  9600  infeq5i  9615  cantnfcl  9646  cardiun  9987  infxpenlem  10016  acnnum  10055  inffien  10066  dfac12lem2  10147  djudoml  10187  cdainflem  10190  djuinf  10191  infunabs  10208  infdju  10209  infdif  10210  infdif2  10211  infmap2  10219  fictb  10246  cofsmo  10271  fin23lem21  10341  hsmexlem1  10428  dmct  10526  mptct  10540  iundomg  10543  iunctb  10577  fpwwe2lem8  10641  canthnum  10652  winalim2  10699  rankcf  10780  tskuni  10786  npomex  10999  hashun2  14439  swrd2lsw  15015  2swrd2eqwrdeq  15016  limsupgord  15549  summolem2  15793  zsum  15795  prodmolem2  16015  zprod  16017  ltoddhalfle  16444  isinv  17842  invsym2  17845  invfun  17846  oppcsect2  17861  oppcinv  17862  efgcpbllemb  19856  frgpuplem  19873  gsumval3  20008  1stcfb  23639  1stcrestlem  23646  2ndcdisj2  23651  txdis1cn  23829  tx1stc  23844  tgphaus  24311  qustgplem  24315  tsmsxp  24349  xmeter  24627  bndth  25154  clmneg1  25278  ovolctb2  25688  ovoliunlem1  25698  i1fd  25877  dvgt0lem2  26199  taylf  26561  efcvx  26649  logccv  26865  loglesqrt  26963  0elold  28140  noseqrdgfn  28536  n0fincut  28585  usgredg2v  29614  crctcshtrl  30209  frgr3vlem1  30661  strlem6  32645  mptctf  33098  omsmeas  34745  sibfof  34762  bnj97  35286  bnj553  35318  bnj966  35364  bnj1442  35469  tz9.1regs  35571  subfaclefac  35689  erdsze2lem1  35716  erdsze2lem2  35717  snmlff  35842  satffunlem2lem2  35919  bj-ssbid2ALT  37326  phpreu  38296  ptrecube  38312  poimirlem3  38315  poimirlem32  38344  heicant  38347  dvhopellsm  41932  aks5lem7  43008  pell1qrgaplem  43641  dnwech  43816  oaun3lem1  44142  mnurndlem1  45032  rn1st  46029  stoweid  46818  dirkercncflem2  46859  fourierdlem36  46898  usgrexmpl12ngric  48844  usgrexmpl12ngrlic  48845