Theorem impel 515

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 35	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	imp 412	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  equs5e  2487  mob2  3672  ssn0rex  4305  reusv2lem2  5360  copsex2t  5463  reuop  6296  trssord  6379  trsuc  6452  funimass2  6624  fvelima  6951  fvmptf  7016  funfvima2  7238  funfvima3  7243  tfi  7865  suppssov1  8218  suppssov2  8219  tposf2  8271  frrlem4  8311  ectocld  8807  mapsnd  8918  resixpfo  8968  f1oeng  9001  nneneq  9225  fodomfi  9308  fiint  9322  eqinf  9481  hartogslem1  9540  cantnf  9698  rankwflemb  9804  rankwflembOLD  9805  rankval4b  9884  carden2a  10051  carduni  10066  harval2  10082  cardaleph  10172  alephval3  10193  dfac5  10211  cfcof  10356  axdc4lem  10537  nqereu  11018  recexsr  11196  seqcoll  14613  swrdswrd  14859  swrdccatin1  14879  swrdccatin2  14883  repswswrd  14940  climcau  15844  odd2np1  16517  lcmfunsnlem2lem2  16820  coprmproddvdslem  16843  dvdsprm  16885  vdwlem6  17170  imasvscafn  17715  dirref  18781  irredn1  20662  isdrng5  21014  isdrngd  21028  isdrngdOLD  21030  psgnghm  21892  gsummoncoe1  22632  prdstopn  23953  cnextcn  24392  tnggrpr  24980  ovolctb  25817  dyadmbl  25927  itg1addlem4  26026  itg1le  26040  dvcnp2  26246  c1liplem1  26322  pserulm  26755  fsumdvdsmul  27528  perfectlem2  27563  dchrisumlem2  27823  noresle  28060  bday1  28206  readdscl  28891  remulscl  28894  axlowdimlem16  29541  wlkv0  30236  wlkp1lem1  30258  wlkswwlksf1o  30474  wspniunwspnon  30518  trlsegvdeglem1  30827  frcond4  30877  2clwwlk2clwwlk  30957  opabssi  33255  nn0xmulclb  33410  zarclsiin  34550  cusgr3cyclex  35988  satfun  36263  fundmpss  36625  nn0prpw  37204  bj-restpw  38106  bj-prmoore  38129  cgsex2gd  38152  domalom  38421  cover2  38743  disjlem18  39929  sticksstones11  43300  setindtr  44125  onov0suclim  44370  oe0suclim  44373  ofoaid1  44454  ofoaid2  44455  naddcnfcom  44462  naddcnfass  44465  omssaxinf2  46072  climxlim2lem  46949  sge0f1o  47486  2reuimp  48279  fvelsetpreimafv  48563  imasetpreimafvbijlemfo  48581  reupr  48698  lighneallem4  48789  proththd  48793  lincresunit3  49687  oppc1stflem  50503