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  2456  mob2  3677  ssn0rex  4311  reusv2lem2  5341  copsex2t  5439  reuop  6245  trssord  6328  trsuc  6400  funimass2  6569  fvelima  6892  fvmptf  6955  funfvima2  7171  funfvima3  7176  tfi  7793  suppssov1  8137  suppssov2  8138  tposf2  8190  frrlem4  8229  ectocld  8716  mapsnd  8820  resixpfo  8870  f1oeng  8903  nneneq  9130  nnsdomgOLD  9205  fodomfi  9219  fiint  9235  fiintOLD  9236  fodomfiOLD  9239  eqinf  9394  hartogslem1  9453  cantnf  9608  rankwflemb  9708  carden2a  9881  carduni  9896  harval2  9912  cardaleph  10002  alephval3  10023  dfac5  10042  cfcof  10187  axdc4lem  10368  nqereu  10842  recexsr  11020  seqcoll  14390  swrdswrd  14630  swrdccatin1  14650  swrdccatin2  14654  repswswrd  14709  climcau  15597  odd2np1  16271  lcmfunsnlem2lem2  16569  coprmproddvdslem  16592  dvdsprm  16633  vdwlem6  16917  imasvscafn  17460  dirref  18526  irredn1  20330  isdrngd  20669  isdrngdOLD  20671  psgnghm  21506  gsummoncoe1  22212  prdstopn  23532  cnextcn  23971  tnggrpr  24560  ovolctb  25408  dyadmbl  25518  itg1addlem4  25617  itg1le  25631  dvcnp2  25838  dvcnp2OLD  25839  c1liplem1  25918  pserulm  26348  fsumdvdsmul  27122  perfectlem2  27158  dchrisumlem2  27418  noresle  27626  bday1s  27764  readdscl  28387  remulscl  28390  axlowdimlem16  28921  wlkv0  29614  wlkp1lem1  29636  wlkswwlksf1o  29843  wspniunwspnon  29887  trlsegvdeglem1  30183  frcond4  30233  2clwwlk2clwwlk  30313  opabssi  32577  nn0xmulclb  32733  zarclsiin  33857  cusgr3cyclex  35128  satfun  35403  fundmpss  35759  nn0prpw  36316  bj-restpw  37085  bj-prmoore  37108  domalom  37397  cover2  37714  disjlem18  38797  sticksstones11  42149  setindtr  43017  onov0suclim  43267  oe0suclim  43270  ofoaid1  43351  ofoaid2  43352  naddcnfcom  43359  naddcnfass  43362  omssaxinf2  44982  climxlim2lem  45846  sge0f1o  46383  2reuimp  47119  fvelsetpreimafv  47391  imasetpreimafvbijlemfo  47409  reupr  47526  lighneallem4  47614  proththd  47618  lincresunit3  48486  oppc1stflem  49292