Theorem impel 508

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 409	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  equs5e  2477  elabgt  3662  mob2  3705  ssn0rex  4314  reusv2lem2  5299  copsex2t  5382  reuop  6143  trssord  6207  trsuc  6274  funimass2  6436  fvelima  6730  fvmptf  6788  funfvima2  6992  funfvima3  6997  tfi  7567  suppssov1  7861  tposf2  7915  wfrlem4  7957  wfrlem10  7963  ectocld  8363  mapsnd  8449  resixpfo  8499  f1oeng  8527  nneneq  8699  nnsdomg  8776  fiint  8794  fodomfi  8796  eqinf  8947  hartogslem1  9005  cantnf  9155  rankwflemb  9221  carden2a  9394  carduni  9409  harval2  9425  cardaleph  9514  alephval3  9535  dfac5  9553  cfcof  9695  axdc4lem  9876  nqereu  10350  recexsr  10528  seqcoll  13821  swrdswrd  14066  swrdccatin1  14086  swrdccatin2  14090  repswswrd  14145  climcau  15026  odd2np1  15689  lcmfunsnlem2lem2  15982  coprmproddvdslem  16005  dvdsprm  16046  vdwlem6  16321  imasvscafn  16809  dirref  17844  irredn1  19455  isdrngd  19526  gsummoncoe1  20471  psgnghm  20723  prdstopn  22235  cnextcn  22674  tnggrpr  23263  ovolctb  24090  dyadmbl  24200  itg1addlem4  24299  itg1le  24313  dvcnp2  24516  c1liplem1  24592  pserulm  25009  perfectlem2  25805  dchrisumlem2  26065  axlowdimlem16  26742  wlkv0  27431  wlkp1lem1  27454  wlkswwlksf1o  27656  wspniunwspnon  27701  trlsegvdeglem1  27998  frcond4  28048  2clwwlk2clwwlk  28128  opabssi  30363  nn0xmulclb  30495  cusgr3cyclex  32383  satfun  32658  fundmpss  33009  frrlem4  33126  noresle  33200  nn0prpw  33671  bj-restpw  34382  bj-prmoore  34406  domalom  34684  cover2  34988  setindtr  39619  climxlim2lem  42124  2reuimp  43313  fvelsetpreimafv  43546  imasetpreimafvbijlemfo  43564  reupr  43683  lighneallem4  43774  proththd  43778  lincresunit3  44535