Theorem impel 513

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  equs5e  2488  mob2  3676  ssn0rex  4308  reusv2lem2  5353  copsex2t  5458  reuop  6275  trssord  6358  trsuc  6430  funimass2  6599  fvelima  6927  fvmptf  6992  funfvima2  7210  funfvima3  7215  tfi  7828  suppssov1  8171  suppssov2  8172  tposf2  8224  frrlem4  8264  ectocld  8758  mapsnd  8862  resixpfo  8912  f1oeng  8945  nneneq  9168  fodomfi  9250  fiint  9265  eqinf  9425  hartogslem1  9484  cantnf  9642  rankwflemb  9745  carden2a  9918  carduni  9933  harval2  9949  cardaleph  10039  alephval3  10060  dfac5  10079  cfcof  10225  axdc4lem  10406  nqereu  10881  recexsr  11059  seqcoll  14471  swrdswrd  14712  swrdccatin1  14732  swrdccatin2  14736  repswswrd  14791  climcau  15689  odd2np1  16366  lcmfunsnlem2lem2  16664  coprmproddvdslem  16687  dvdsprm  16729  vdwlem6  17013  imasvscafn  17558  dirref  18624  irredn1  20462  isdrngd  20802  isdrngdOLD  20804  psgnghm  21620  gsummoncoe1  22359  prdstopn  23676  cnextcn  24115  tnggrpr  24703  ovolctb  25540  dyadmbl  25650  itg1addlem4  25749  itg1le  25763  dvcnp2  25970  c1liplem1  26046  pserulm  26473  fsumdvdsmul  27247  perfectlem2  27282  dchrisumlem2  27542  noresle  27749  bday1  27895  readdscl  28580  remulscl  28583  axlowdimlem16  29115  wlkv0  29807  wlkp1lem1  29829  wlkswwlksf1o  30036  wspniunwspnon  30080  trlsegvdeglem1  30379  frcond4  30429  2clwwlk2clwwlk  30509  opabssi  32776  nn0xmulclb  32934  zarclsiin  34129  rankval4b  35357  cusgr3cyclex  35447  satfun  35722  fundmpss  36078  nn0prpw  36644  bj-restpw  37543  bj-prmoore  37566  cgsex2gd  37590  domalom  37859  cover2  38175  disjlem18  39363  sticksstones11  42734  setindtr  43562  onov0suclim  43812  oe0suclim  43815  ofoaid1  43896  ofoaid2  43897  naddcnfcom  43904  naddcnfass  43907  omssaxinf2  45525  climxlim2lem  46380  sge0f1o  46917  2reuimp  47670  fvelsetpreimafv  47954  imasetpreimafvbijlemfo  47972  reupr  48089  lighneallem4  48180  proththd  48184  lincresunit3  49064  oppc1stflem  49869