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  2460  mob2  3670  ssn0rex  4307  reusv2lem2  5341  copsex2t  5437  reuop  6248  trssord  6331  trsuc  6403  funimass2  6572  fvelima  6896  fvmptf  6959  funfvima2  7174  funfvima3  7179  tfi  7792  suppssov1  8136  suppssov2  8137  tposf2  8189  frrlem4  8228  ectocld  8715  mapsnd  8820  resixpfo  8870  f1oeng  8903  nneneq  9126  fodomfi  9207  fiint  9222  fodomfiOLD  9225  eqinf  9380  hartogslem1  9439  cantnf  9594  rankwflemb  9697  carden2a  9870  carduni  9885  harval2  9901  cardaleph  9991  alephval3  10012  dfac5  10031  cfcof  10176  axdc4lem  10357  nqereu  10831  recexsr  11009  seqcoll  14378  swrdswrd  14619  swrdccatin1  14639  swrdccatin2  14643  repswswrd  14698  climcau  15585  odd2np1  16259  lcmfunsnlem2lem2  16557  coprmproddvdslem  16580  dvdsprm  16621  vdwlem6  16905  imasvscafn  17449  dirref  18515  irredn1  20353  isdrngd  20689  isdrngdOLD  20691  psgnghm  21526  gsummoncoe1  22243  prdstopn  23563  cnextcn  24002  tnggrpr  24590  ovolctb  25438  dyadmbl  25548  itg1addlem4  25647  itg1le  25661  dvcnp2  25868  dvcnp2OLD  25869  c1liplem1  25948  pserulm  26378  fsumdvdsmul  27152  perfectlem2  27188  dchrisumlem2  27448  noresle  27656  bday1s  27795  readdscl  28421  remulscl  28424  axlowdimlem16  28956  wlkv0  29649  wlkp1lem1  29671  wlkswwlksf1o  29878  wspniunwspnon  29922  trlsegvdeglem1  30221  frcond4  30271  2clwwlk2clwwlk  30351  opabssi  32617  nn0xmulclb  32779  zarclsiin  33956  rankval4b  35183  cusgr3cyclex  35252  satfun  35527  fundmpss  35883  nn0prpw  36439  bj-restpw  37209  bj-prmoore  37232  domalom  37521  cover2  37828  disjlem18  38971  sticksstones11  42322  setindtr  43181  onov0suclim  43431  oe0suclim  43434  ofoaid1  43515  ofoaid2  43516  naddcnfcom  43523  naddcnfass  43526  omssaxinf2  45145  climxlim2lem  46005  sge0f1o  46542  2reuimp  47277  fvelsetpreimafv  47549  imasetpreimafvbijlemfo  47567  reupr  47684  lighneallem4  47772  proththd  47776  lincresunit3  48643  oppc1stflem  49448