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  3698  ssn0rex  4333  reusv2lem2  5369  copsex2t  5467  reuop  6282  trssord  6369  trsuc  6440  funimass2  6618  fvelima  6943  fvmptf  7006  funfvima2  7222  funfvima3  7227  tfi  7846  suppssov1  8194  suppssov2  8195  tposf2  8247  frrlem4  8286  wfrlem4OLD  8324  wfrlem10OLD  8330  ectocld  8796  mapsnd  8898  resixpfo  8948  f1oeng  8983  nneneq  9218  nnsdomgOLD  9306  fodomfi  9320  fiint  9336  fiintOLD  9337  fodomfiOLD  9340  eqinf  9495  hartogslem1  9554  cantnf  9705  rankwflemb  9805  carden2a  9978  carduni  9993  harval2  10009  cardaleph  10101  alephval3  10122  dfac5  10141  cfcof  10286  axdc4lem  10467  nqereu  10941  recexsr  11119  seqcoll  14480  swrdswrd  14721  swrdccatin1  14741  swrdccatin2  14745  repswswrd  14800  climcau  15685  odd2np1  16358  lcmfunsnlem2lem2  16656  coprmproddvdslem  16679  dvdsprm  16720  vdwlem6  17004  imasvscafn  17549  dirref  18609  irredn1  20384  isdrngd  20723  isdrngdOLD  20725  psgnghm  21538  gsummoncoe1  22244  prdstopn  23564  cnextcn  24003  tnggrpr  24592  ovolctb  25441  dyadmbl  25551  itg1addlem4  25650  itg1le  25664  dvcnp2  25871  dvcnp2OLD  25872  c1liplem1  25951  pserulm  26381  fsumdvdsmul  27155  perfectlem2  27191  dchrisumlem2  27451  noresle  27659  bday1s  27793  readdscl  28348  remulscl  28351  axlowdimlem16  28882  wlkv0  29577  wlkp1lem1  29599  wlkswwlksf1o  29807  wspniunwspnon  29851  trlsegvdeglem1  30147  frcond4  30197  2clwwlk2clwwlk  30277  opabssi  32539  nn0xmulclb  32694  zarclsiin  33848  cusgr3cyclex  35104  satfun  35379  fundmpss  35730  nn0prpw  36287  bj-restpw  37056  bj-prmoore  37079  domalom  37368  cover2  37685  disjlem18  38764  sticksstones11  42115  setindtr  42995  onov0suclim  43245  oe0suclim  43248  ofoaid1  43329  ofoaid2  43330  naddcnfcom  43337  naddcnfass  43340  omssaxinf2  44961  climxlim2lem  45822  sge0f1o  46359  2reuimp  47092  fvelsetpreimafv  47349  imasetpreimafvbijlemfo  47367  reupr  47484  lighneallem4  47572  proththd  47576  lincresunit3  48405