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  3673  ssn0rex  4310  reusv2lem2  5344  copsex2t  5440  reuop  6251  trssord  6334  trsuc  6406  funimass2  6575  fvelima  6899  fvmptf  6962  funfvima2  7177  funfvima3  7182  tfi  7795  suppssov1  8139  suppssov2  8140  tposf2  8192  frrlem4  8231  ectocld  8719  mapsnd  8824  resixpfo  8874  f1oeng  8907  nneneq  9130  fodomfi  9212  fiint  9227  fodomfiOLD  9230  eqinf  9388  hartogslem1  9447  cantnf  9602  rankwflemb  9705  carden2a  9878  carduni  9893  harval2  9909  cardaleph  9999  alephval3  10020  dfac5  10039  cfcof  10184  axdc4lem  10365  nqereu  10840  recexsr  11018  seqcoll  14387  swrdswrd  14628  swrdccatin1  14648  swrdccatin2  14652  repswswrd  14707  climcau  15594  odd2np1  16268  lcmfunsnlem2lem2  16566  coprmproddvdslem  16589  dvdsprm  16630  vdwlem6  16914  imasvscafn  17458  dirref  18524  irredn1  20362  isdrngd  20698  isdrngdOLD  20700  psgnghm  21535  gsummoncoe1  22252  prdstopn  23572  cnextcn  24011  tnggrpr  24599  ovolctb  25447  dyadmbl  25557  itg1addlem4  25656  itg1le  25670  dvcnp2  25877  dvcnp2OLD  25878  c1liplem1  25957  pserulm  26387  fsumdvdsmul  27161  perfectlem2  27197  dchrisumlem2  27457  noresle  27665  bday1  27810  readdscl  28495  remulscl  28498  axlowdimlem16  29030  wlkv0  29723  wlkp1lem1  29745  wlkswwlksf1o  29952  wspniunwspnon  29996  trlsegvdeglem1  30295  frcond4  30345  2clwwlk2clwwlk  30425  opabssi  32691  nn0xmulclb  32851  zarclsiin  34028  rankval4b  35256  cusgr3cyclex  35330  satfun  35605  fundmpss  35961  nn0prpw  36517  bj-restpw  37297  bj-prmoore  37320  domalom  37609  cover2  37916  disjlem18  39059  sticksstones11  42410  setindtr  43266  onov0suclim  43516  oe0suclim  43519  ofoaid1  43600  ofoaid2  43601  naddcnfcom  43608  naddcnfass  43611  omssaxinf2  45229  climxlim2lem  46089  sge0f1o  46626  2reuimp  47361  fvelsetpreimafv  47633  imasetpreimafvbijlemfo  47651  reupr  47768  lighneallem4  47856  proththd  47860  lincresunit3  48727  oppc1stflem  49532