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  3673  fvsng  7182  fveqf1o  7307  fliftcnv  7316  fliftfun  7317  frxp3  8153  orderseqlem  8159  cnvct  9045  pwdom  9131  php  9205  ordiso  9492  ordtypelem8  9501  wdompwdom  9554  unxpwdom  9565  harwdom  9567  inf0  9604  infeq5i  9619  cantnfcl  9650  cardiun  9991  infxpenlem  10020  acnnum  10059  inffien  10070  dfac12lem2  10151  djudoml  10191  cdainflem  10194  djuinf  10195  infunabs  10212  infdju  10213  infdif  10214  infdif2  10215  infmap2  10223  fictb  10250  cofsmo  10275  fin23lem21  10345  hsmexlem1  10432  dmct  10530  dmctOLD  10531  mptct  10550  iundomg  10553  iunctb  10587  fpwwe2lem8  10651  canthnum  10662  winalim2  10709  rankcf  10790  tskuni  10796  npomex  11009  hashun2  14451  swrd2lsw  15029  2swrd2eqwrdeq  15030  limsupgord  15563  summolem2  15806  zsum  15808  prodmolem2  16028  zprod  16030  ltoddhalfle  16457  isinv  17855  invsym2  17858  invfun  17859  oppcsect2  17874  oppcinv  17875  efgcpbllemb  19888  frgpuplem  19905  gsumval3  20040  1stcfb  23676  1stcrestlem  23683  2ndcdisj2  23689  txdis1cn  23867  tx1stc  23882  tgphaus  24349  qustgplem  24353  tsmsxp  24387  xmeter  24665  bndth  25192  clmneg1  25316  ovolctb2  25726  ovoliunlem1  25736  i1fd  25915  dvgt0lem2  26237  taylf  26604  efcvx  26692  logccv  26908  loglesqrt  27006  0elold  28183  noseqrdgfn  28579  n0fincut  28628  usgredg2v  29695  crctcshtrl  30299  frgr3vlem1  30761  strlem6  32745  mptctf  33195  omsmeas  34842  sibfof  34859  bnj97  35383  bnj553  35415  bnj966  35461  bnj1442  35566  tz9.1regs  35668  subfaclefac  35763  erdsze2lem1  35790  erdsze2lem2  35791  snmlff  35916  satffunlem2lem2  35993  bj-ssbid2ALT  37401  phpreu  38366  ptrecube  38377  poimirlem3  38380  poimirlem32  38409  heicant  38412  dvhopellsm  41998  aks5lem7  43074  pell1qrgaplem  43722  dnwech  43897  oaun3lem1  44223  mnurndlem1  45113  rn1st  46110  stoweid  46899  dirkercncflem2  46940  fourierdlem36  46979  usgrexmpl12ngric  48962  usgrexmpl12ngrlic  48963