Theorem impel 505

Description: An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)

Hypotheses

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

Assertion

Ref	Expression
impel	⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Proof of Theorem impel

Step	Hyp	Ref	Expression
1		impel.2	. . 3 ⊢ (𝜃 → 𝜓)
2		impel.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	imp 406	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  equs5e  2462  mob2  3661  ssn0rex  4298  reusv2lem2  5341  copsex2t  5446  reuop  6257  trssord  6340  trsuc  6412  funimass2  6581  fvelima  6905  fvmptf  6969  funfvima2  7186  funfvima3  7191  tfi  7804  suppssov1  8147  suppssov2  8148  tposf2  8200  frrlem4  8239  ectocld  8729  mapsnd  8834  resixpfo  8884  f1oeng  8917  nneneq  9140  fodomfi  9222  fiint  9237  fodomfiOLD  9240  eqinf  9398  hartogslem1  9457  cantnf  9614  rankwflemb  9717  carden2a  9890  carduni  9905  harval2  9921  cardaleph  10011  alephval3  10032  dfac5  10051  cfcof  10196  axdc4lem  10377  nqereu  10852  recexsr  11030  seqcoll  14426  swrdswrd  14667  swrdccatin1  14687  swrdccatin2  14691  repswswrd  14746  climcau  15633  odd2np1  16310  lcmfunsnlem2lem2  16608  coprmproddvdslem  16631  dvdsprm  16673  vdwlem6  16957  imasvscafn  17501  dirref  18567  irredn1  20406  isdrngd  20742  isdrngdOLD  20744  psgnghm  21560  gsummoncoe1  22273  prdstopn  23593  cnextcn  24032  tnggrpr  24620  ovolctb  25457  dyadmbl  25567  itg1addlem4  25666  itg1le  25680  dvcnp2  25887  c1liplem1  25963  pserulm  26387  fsumdvdsmul  27158  perfectlem2  27193  dchrisumlem2  27453  noresle  27661  bday1  27806  readdscl  28491  remulscl  28494  axlowdimlem16  29026  wlkv0  29718  wlkp1lem1  29740  wlkswwlksf1o  29947  wspniunwspnon  29991  trlsegvdeglem1  30290  frcond4  30340  2clwwlk2clwwlk  30420  opabssi  32686  nn0xmulclb  32844  zarclsiin  34015  rankval4b  35243  cusgr3cyclex  35318  satfun  35593  fundmpss  35949  nn0prpw  36505  bj-restpw  37404  bj-prmoore  37427  cgsex2gd  37451  domalom  37720  cover2  38036  disjlem18  39224  sticksstones11  42595  setindtr  43452  onov0suclim  43702  oe0suclim  43705  ofoaid1  43786  ofoaid2  43787  naddcnfcom  43794  naddcnfass  43797  omssaxinf2  45415  climxlim2lem  46273  sge0f1o  46810  2reuimp  47563  fvelsetpreimafv  47847  imasetpreimafvbijlemfo  47865  reupr  47982  lighneallem4  48073  proththd  48077  lincresunit3  48957  oppc1stflem  49762