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  2463  mob2  3721  ssn0rex  4358  reusv2lem2  5399  copsex2t  5497  reuop  6313  trssord  6401  trsuc  6471  funimass2  6649  fvelima  6974  fvmptf  7037  funfvima2  7251  funfvima3  7256  tfi  7874  suppssov1  8222  suppssov2  8223  tposf2  8275  frrlem4  8314  wfrlem4OLD  8352  wfrlem10OLD  8358  ectocld  8824  mapsnd  8926  resixpfo  8976  f1oeng  9011  nneneq  9246  nneneqOLD  9258  nnsdomgOLD  9336  fodomfi  9350  fiint  9366  fiintOLD  9367  fodomfiOLD  9370  eqinf  9524  hartogslem1  9582  cantnf  9733  rankwflemb  9833  carden2a  10006  carduni  10021  harval2  10037  cardaleph  10129  alephval3  10150  dfac5  10169  cfcof  10314  axdc4lem  10495  nqereu  10969  recexsr  11147  seqcoll  14503  swrdswrd  14743  swrdccatin1  14763  swrdccatin2  14767  repswswrd  14822  climcau  15707  odd2np1  16378  lcmfunsnlem2lem2  16676  coprmproddvdslem  16699  dvdsprm  16740  vdwlem6  17024  imasvscafn  17582  dirref  18646  irredn1  20426  isdrngd  20765  isdrngdOLD  20767  psgnghm  21598  gsummoncoe1  22312  prdstopn  23636  cnextcn  24075  tnggrpr  24676  ovolctb  25525  dyadmbl  25635  itg1addlem4  25734  itg1le  25748  dvcnp2  25955  dvcnp2OLD  25956  c1liplem1  26035  pserulm  26465  fsumdvdsmul  27238  perfectlem2  27274  dchrisumlem2  27534  noresle  27742  bday1s  27876  readdscl  28431  remulscl  28434  axlowdimlem16  28972  wlkv0  29669  wlkp1lem1  29691  wlkswwlksf1o  29899  wspniunwspnon  29943  trlsegvdeglem1  30239  frcond4  30289  2clwwlk2clwwlk  30369  opabssi  32625  nn0xmulclb  32775  zarclsiin  33870  cusgr3cyclex  35141  satfun  35416  fundmpss  35767  nn0prpw  36324  bj-restpw  37093  bj-prmoore  37116  domalom  37405  cover2  37722  disjlem18  38801  sticksstones11  42157  setindtr  43036  onov0suclim  43287  oe0suclim  43290  ofoaid1  43371  ofoaid2  43372  naddcnfcom  43379  naddcnfass  43382  omssaxinf2  45005  climxlim2lem  45860  sge0f1o  46397  2reuimp  47127  fvelsetpreimafv  47374  imasetpreimafvbijlemfo  47392  reupr  47509  lighneallem4  47597  proththd  47601  lincresunit3  48398